Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-13 21:34 3b5edd06

View on Github →

refactor(set_theory/cardinal_ordinal): use TC assumptions instead of inequalities (#10313) Assume [fintype α] or [infinite α] instead of #α < ω or ω ≤ #α.

Estimated changes

Modified src/set_theory/cardinal_ordinal.lean

modified theorem cardinal.extend_function_finite

added theorem cardinal.mk_bounded_set_le_of_infinite

deleted theorem cardinal.mk_bounded_set_le_of_omega_le

modified theorem cardinal.mk_compl_eq_mk_compl_finite

modified theorem cardinal.mk_compl_eq_mk_compl_finite_lift

modified theorem cardinal.mk_compl_eq_mk_compl_finite_same

modified theorem cardinal.mk_compl_eq_mk_compl_infinite

added theorem cardinal.mk_compl_finset_of_infinite

deleted theorem cardinal.mk_compl_finset_of_omega_le

added theorem cardinal.mk_compl_of_infinite

deleted theorem cardinal.mk_compl_of_omega_le

modified theorem cardinal.powerlt_omega