Preskoči na glavno vsebino

Andrej Bauer: Formalizacija realnih števil 2

Datum objave: 25. 11. 2013
Seminar za temelje matematike in teoretično računalništvo
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).