Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-18 02:27 a8f2bab2

View on Github →

chore(set_theory/cardinal): use notation #, add notation ω (#9217) The only API change: rename cardinal.eq_congr to cardinal.mk_congr.

Estimated changes

modified theorem two_le_mk_bcubes
modified theorem cardinal.mk_rat
modified theorem dim_span_le
modified theorem finsupp.dim_eq
modified theorem cardinal.add_def
modified theorem cardinal.add_lt_omega
modified theorem cardinal.add_lt_omega_iff
modified theorem cardinal.countable_iff
modified theorem cardinal.denumerable_iff
modified theorem cardinal.finset_card
modified theorem cardinal.fintype_card
modified theorem cardinal.infinite_iff
modified theorem cardinal.le_def
modified theorem cardinal.lift_mk
modified theorem cardinal.lift_mk_fin
modified theorem cardinal.lift_omega
modified theorem cardinal.lt_omega
modified theorem cardinal.mk_Prop
modified theorem cardinal.mk_Union_le_sum_mk
modified theorem cardinal.mk_bool
modified theorem cardinal.mk_def
modified theorem cardinal.mk_empty
modified theorem cardinal.mk_emptyc
modified theorem cardinal.mk_emptyc_iff
modified theorem cardinal.mk_fin
modified theorem cardinal.mk_image_le
modified theorem cardinal.mk_int
modified theorem cardinal.mk_le_mk_of_subset
modified theorem cardinal.mk_le_of_injective
modified theorem cardinal.mk_list_eq_sum_pow
modified theorem cardinal.mk_nat
modified theorem cardinal.mk_option
modified theorem cardinal.mk_out
modified theorem cardinal.mk_pempty
modified theorem cardinal.mk_plift_of_false
modified theorem cardinal.mk_plift_of_true
modified theorem cardinal.mk_pnat
modified theorem cardinal.mk_punit
modified theorem cardinal.mk_quot_le
modified theorem cardinal.mk_quotient_le
modified theorem cardinal.mk_range_eq
modified theorem cardinal.mk_range_le
modified theorem cardinal.mk_sep
modified theorem cardinal.mk_set
modified theorem cardinal.mk_set_le
modified theorem cardinal.mk_singleton
modified theorem cardinal.mk_subtype_le
modified theorem cardinal.mk_subtype_mono
modified theorem cardinal.mk_to_nat_eq_card
modified theorem cardinal.mk_union_le
modified theorem cardinal.mk_unit
modified theorem cardinal.mk_univ
modified theorem cardinal.mul_def
modified theorem cardinal.mul_lt_omega
modified theorem cardinal.mul_lt_omega_iff
modified theorem cardinal.nat_lt_omega
modified def cardinal.omega
modified theorem cardinal.omega_le
modified theorem cardinal.omega_ne_zero
modified theorem cardinal.omega_pos
modified theorem cardinal.one_lt_omega
modified theorem cardinal.power_def
modified theorem cardinal.power_lt_omega
modified def cardinal.prod
modified theorem cardinal.prod_const
modified theorem cardinal.prod_mk
modified theorem cardinal.prop_eq_two
modified theorem cardinal.sum_const
modified theorem cardinal.sum_le_sup
modified theorem cardinal.sum_mk
modified theorem cardinal.two_le_iff'
modified theorem cardinal.two_le_iff
deleted theorem equiv.cardinal_eq
modified theorem cardinal.mk_cardinal
modified theorem cardinal.mk_finset_eq_mk
modified theorem cardinal.mk_list_eq_mk
modified theorem cardinal.lt_cof_power
modified theorem cardinal.lt_power_cof
modified theorem cardinal.omega_is_regular
modified theorem cardinal.succ_is_regular
modified theorem ordinal.cof_omega
modified theorem ordinal.infinite_pigeonhole
modified theorem ordinal.lt_cof_type
modified theorem ordinal.omega_le_cof
modified theorem ordinal.sup_lt
modified theorem ordinal.sup_lt_ord
modified theorem cardinal.mk_ord_out
modified theorem cardinal.ord_eq_min
modified theorem cardinal.ord_le_type
modified def cardinal.univ
modified theorem cardinal.univ_id