Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-02 04:28 37c31209

View on Github →

feat(set_theory/ordinal_notation): ordinal notations for ordinals < e0 This allows us to compute with small countable ordinals using trees of nats.

Estimated changes

modified theorem lt_iff_lt_of_strict_mono
added theorem ordering.compares.inj
modified theorem nat.cast_add_one
modified def nat.succ_pnat
modified def nat.to_pnat'
modified def nat.to_pnat
modified theorem pnat.nat_coe_val
added theorem pnat.ne_zero
modified theorem pnat.to_pnat'_coe
modified theorem pnat.to_pnat'_val
added theorem imp_or_distrib'
added theorem imp_or_distrib
added theorem ordinal.add_mul_limit
added theorem ordinal.add_mul_succ
added theorem ordinal.bsup_type
added theorem ordinal.cof_bsup_le
added theorem ordinal.nat_cast_pos
added def nonote.cmp
added theorem nonote.cmp_compares
added def nonote.of_nat
added theorem nonote.repr_add
added theorem nonote.repr_mul
added def nonote
added theorem onote.NF.below_of_lt
added theorem onote.NF.fst
added theorem onote.NF.oadd
added theorem onote.NF.snd'
added theorem onote.NF.snd
added theorem onote.NF.zero
added def onote.NF
added theorem onote.NF_below.fst
added theorem onote.NF_below.lt
added theorem onote.NF_below.mono
added theorem onote.NF_below.oadd
added theorem onote.NF_below.repr_lt
added theorem onote.NF_below.snd
added inductive onote.NF_below
added theorem onote.NF_below_of_nat
added theorem onote.NF_below_zero
added theorem onote.NF_of_nat
added def onote.add
added theorem onote.add_NF
added theorem onote.add_NF_below
added def onote.cmp
added theorem onote.cmp_compares
added theorem onote.eq_of_cmp_eq
added theorem onote.le_def
added theorem onote.lt_def
added def onote.mul
added theorem onote.mul_NF
added theorem onote.oadd_lt_oadd_1
added theorem onote.oadd_lt_oadd_2
added theorem onote.oadd_lt_oadd_3
added theorem onote.oadd_pos
added def onote.of_nat
added theorem onote.of_nat_one
added theorem onote.omega_le_oadd
added def onote.power
added def onote.power_aux
added theorem onote.repr_add
added theorem onote.repr_inj
added theorem onote.repr_mul
added theorem onote.repr_of_nat
added theorem onote.repr_one
added def onote.scale
added def onote.split'
added def onote.split
added def onote.sub
added def onote.top_below
added theorem onote.zero_def
added theorem onote.zero_lt_one
added inductive onote