Commit 2023-06-21 05:19 7eebe3d2

View on Github →

feat: port SetTheory.Ordinal.Notation (#2470)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Ordinal/Notation.lean

added def NONote.below

added def NONote.cmp

added theorem NONote.cmp_compares

added theorem NONote.lt_wf

added def NONote.mk

added def NONote.oadd

added def NONote.ofNat

added def NONote.opow

added def NONote.recOn

added theorem NONote.repr_add

added theorem NONote.repr_mul

added theorem NONote.repr_opow

added theorem NONote.repr_sub

added def NONote

added def ONote.FundamentalSequenceProp

added theorem ONote.NF.below_of_lt'

added theorem ONote.NF.below_of_lt

added theorem ONote.NF.fst

added theorem ONote.NF.oadd

added theorem ONote.NF.of_dvd_omega

added theorem ONote.NF.of_dvd_omega_opow

added theorem ONote.NF.snd'

added theorem ONote.NF.snd

added theorem ONote.NF.zero_of_zero

added theorem ONote.NFBelow.fst

added theorem ONote.NFBelow.lt

added theorem ONote.NFBelow.mono

added theorem ONote.NFBelow.oadd

added theorem ONote.NFBelow.repr_lt

added theorem ONote.NFBelow.snd

added inductive ONote.NFBelow

added theorem ONote.NFBelow_zero

added def ONote.TopBelow

added def ONote.add

added def ONote.addAux

added theorem ONote.add_nfBelow

added def ONote.cmp

added theorem ONote.cmp_compares

added theorem ONote.eq_of_cmp_eq

added def ONote.fastGrowing

added theorem ONote.fastGrowing_def

added theorem ONote.fastGrowing_limit

added theorem ONote.fastGrowing_one

added theorem ONote.fastGrowing_succ

added theorem ONote.fastGrowing_two

added theorem ONote.fastGrowing_zero'

added theorem ONote.fastGrowing_zero

added def ONote.fastGrowingε₀

added theorem ONote.fastGrowingε₀_one

added theorem ONote.fastGrowingε₀_two

added theorem ONote.fastGrowingε₀_zero

added def ONote.fundamentalSequence

added theorem ONote.fundamentalSequenceProp_inl_none

added theorem ONote.fundamentalSequenceProp_inl_some

added theorem ONote.fundamentalSequenceProp_inr

added theorem ONote.fundamentalSequence_has_prop

added theorem ONote.le_def

added theorem ONote.lt_def

added def ONote.mul

added def ONote.mulNat

added theorem ONote.mulNat_eq_mul

added theorem ONote.nfBelow_iff_topBelow

added theorem ONote.nfBelow_ofNat

added theorem ONote.nf_repr_split'

added theorem ONote.nf_repr_split

added theorem ONote.oadd_add

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_mul

added theorem ONote.oadd_mul_nfBelow

added theorem ONote.oadd_pos

added def ONote.ofNat

added theorem ONote.ofNat_one

added theorem ONote.ofNat_succ

added theorem ONote.ofNat_zero

added def ONote.omega

added theorem ONote.omega_le_oadd

added def ONote.opow

added def ONote.opowAux2

added def ONote.opowAux

added theorem ONote.opow_def

added def ONote.repr'

added theorem ONote.repr_add

added theorem ONote.repr_inj

added theorem ONote.repr_mul

added theorem ONote.repr_ofNat

added theorem ONote.repr_one

added theorem ONote.repr_opow

added theorem ONote.repr_opow_aux₁

added theorem ONote.repr_opow_aux₂

added theorem ONote.repr_scale

added theorem ONote.repr_sub

added def ONote.scale

added theorem ONote.scale_eq_mul

added theorem ONote.scale_opowAux

added def ONote.split'

added def ONote.split

added theorem ONote.split_add_lt

added theorem ONote.split_dvd

added theorem ONote.split_eq_scale_split'

added def ONote.sub

added theorem ONote.sub_nfBelow

added def ONote.toString

added def ONote.toStringAux1

added theorem ONote.zero_add

added theorem ONote.zero_def

added inductive ONote