Commit 2023-02-18 20:14 23670723

View on Github →

Port/SetTheory.Ordinal.NaturalOps (#2353)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean

Created Mathlib/SetTheory/Ordinal/NaturalOps.lean

added theorem NatOrdinal.add_one_eq_succ

added theorem NatOrdinal.induction

added theorem NatOrdinal.lt_wf

added theorem NatOrdinal.succ_def

added def NatOrdinal.toOrdinal

added theorem NatOrdinal.toOrdinal_cast_nat

added theorem NatOrdinal.toOrdinal_eq_one

added theorem NatOrdinal.toOrdinal_eq_zero

added theorem NatOrdinal.toOrdinal_max

added theorem NatOrdinal.toOrdinal_min

added theorem NatOrdinal.toOrdinal_one

added theorem NatOrdinal.toOrdinal_symm_eq

added theorem NatOrdinal.toOrdinal_toNatOrdinal

added theorem NatOrdinal.toOrdinal_zero

added def NatOrdinal

added theorem Ordinal.add_le_nadd

added theorem Ordinal.blsub_nadd_of_mono

added theorem Ordinal.le_of_nadd_le_nadd_left

added theorem Ordinal.le_of_nadd_le_nadd_right

added theorem Ordinal.lt_nadd_iff

added theorem Ordinal.lt_of_nadd_lt_nadd_left

added theorem Ordinal.lt_of_nadd_lt_nadd_right

added theorem Ordinal.nadd_assoc

added theorem Ordinal.nadd_comm

added theorem Ordinal.nadd_def

added theorem Ordinal.nadd_le_iff

added theorem Ordinal.nadd_le_nadd_iff_left

added theorem Ordinal.nadd_le_nadd_iff_right

added theorem Ordinal.nadd_le_nadd_left

added theorem Ordinal.nadd_le_nadd_right

added theorem Ordinal.nadd_left_cancel

added theorem Ordinal.nadd_left_cancel_iff

added theorem Ordinal.nadd_lt_nadd_iff_left

added theorem Ordinal.nadd_lt_nadd_iff_right

added theorem Ordinal.nadd_lt_nadd_left

added theorem Ordinal.nadd_lt_nadd_right

added theorem Ordinal.nadd_nat

added theorem Ordinal.nadd_one

added theorem Ordinal.nadd_right_cancel

added theorem Ordinal.nadd_right_cancel_iff

added theorem Ordinal.nadd_succ

added theorem Ordinal.nadd_zero

added theorem Ordinal.nat_nadd

added theorem Ordinal.one_nadd

added theorem Ordinal.succ_nadd

added def Ordinal.toNatOrdinal

added theorem Ordinal.toNatOrdinal_cast_nat

added theorem Ordinal.toNatOrdinal_eq_one

added theorem Ordinal.toNatOrdinal_eq_zero

added theorem Ordinal.toNatOrdinal_max

added theorem Ordinal.toNatOrdinal_min

added theorem Ordinal.toNatOrdinal_one

added theorem Ordinal.toNatOrdinal_symm_eq

added theorem Ordinal.toNatOrdinal_toOrdinal

added theorem Ordinal.toNatOrdinal_zero

added theorem Ordinal.zero_nadd