Commit 2022-02-15 15:52 721bace8

View on Github →

refactor(set_theory/ordinal_arithmetic): omin → Inf (#11867) We remove the redundant omin in favor of Inf. We also introduce a conditionally_complete_linear_order_bot instance on cardinals, and golf a particularly messy proof.

Estimated changes

Modified src/set_theory/cardinal.lean

added def cardinal.min

added def cardinal.out_mk_equiv

added def cardinal.powerlt

added def cardinal.succ

added def cardinal.sup

added def cardinal.to_enat

added def cardinal.to_nat

Modified src/set_theory/cardinal_ordinal.lean

modified theorem cardinal.ord_aleph'_eq_enum_card

modified theorem cardinal.ord_aleph_eq_enum_card

Modified src/set_theory/game/nim.lean

Modified src/set_theory/ordinal.lean

deleted theorem ordinal.Inf_eq_omin

deleted theorem ordinal.Inf_mem

deleted theorem ordinal.le_omin

deleted theorem ordinal.not_lt_omin

deleted def ordinal.omin

deleted theorem ordinal.omin_le

deleted theorem ordinal.omin_mem

Modified src/set_theory/ordinal_arithmetic.lean

modified theorem ordinal.blsub_le_enum_ord

modified theorem ordinal.deriv_eq_enum_fp

modified theorem ordinal.div_def

added theorem ordinal.div_nonempty

modified theorem ordinal.div_zero

modified def ordinal.enum_ord.order_iso

modified theorem ordinal.enum_ord.strict_mono

modified theorem ordinal.enum_ord.surjective

modified def ordinal.enum_ord

deleted theorem ordinal.enum_ord_def'_H

added theorem ordinal.enum_ord_def'_nonempty

deleted theorem ordinal.enum_ord_def_H

added theorem ordinal.enum_ord_def_nonempty

modified theorem ordinal.enum_ord_mem

modified theorem ordinal.enum_ord_range

added theorem ordinal.enum_ord_succ_le

added theorem ordinal.enum_ord_zero

added theorem ordinal.enum_ord_zero_le

modified theorem ordinal.eq_enum_ord

modified theorem ordinal.log_def

added theorem ordinal.log_nonempty

added theorem ordinal.sub_nonempty

modified theorem ordinal.succ_log_def

modified def ordinal.sup

added theorem ordinal.sup_nonempty