Skip to main content

Andrej Bauer: Formalizacija realnih števil 2

Date of publication: 25. 11. 2013
Mathematics and theoretical computing seminar
Torek, 26. 11. 2013, od 12h do 14h, Plemljev seminar, Jadranska 19
Povzetek: Nadaljevali bomo s formalizacijo realnih števil. Tokrat se bomo posvetili Lipschitozvim funkcijam, ki jih bomo formalizirali s pomočjo razrednih tipov (type classes). Še prej bomo formalizirali metrične prostore z racionalno metriko (tako, ki zavzema vrednosti na racionalnih številih).