Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-04 19:37 10da8e67

View on Github →

feat(set_theory/cardinal,*): assorted lemmas (#9516)

New instances

  • a denumerable type is infinite;
  • Prop is (noncomputably) enumerable;
  • Prop is nontrivial;
  • cardinal.can_lift_cardinal_Type: lift cardinal.{u} to Type u.

New lemmas / attrs

  • quotient.out_equiv_out : x.out ≈ y.out ↔ x = y;
  • quotient.out_inj : x.out = y.out ↔ x = y;
  • cardinal.lift_bit0, cardinal.lift_bit1, cardinal.lift_two, cardinal.lift_prod : new lemmas about cardinal.lift;
  • cardinal.omega_le_lift and cardinal.lift_le_omega : simplify ω ≤ lift c and lift c ≤ ω;
  • cardinal.omega_le_add_iff, cardinal.encodable_iff, cardinal.mk_le_omega, cardinal.mk_denumerable: new lemmas about cardinal.omega;
  • add @[simp] attribute to cardinal.mk_univ, add cardinal.mk_insert;
  • generalize cardinal.nat_power_eq to cardinal.power_eq_two_power and cardinal.prod_eq_two_power.

Estimated changes

added theorem quotient.out_equiv_out
added theorem quotient.out_inj
modified theorem cardinal.mk_rat
added theorem cardinal.encodable_iff
added theorem cardinal.lift_bit0
added theorem cardinal.lift_bit1
added theorem cardinal.lift_le_omega
added theorem cardinal.lift_prod
added theorem cardinal.lift_two
modified theorem cardinal.lift_two_power
added theorem cardinal.mk_insert
modified theorem cardinal.mk_int
added theorem cardinal.mk_le_omega
modified theorem cardinal.mk_nat
modified theorem cardinal.mk_pnat
modified theorem cardinal.mk_univ
added theorem cardinal.omega_le_lift
added theorem cardinal.omega_le_mk
modified theorem cardinal.nat_power_eq
modified theorem cardinal.pow_le
modified theorem cardinal.power_nat_le
modified theorem cardinal.power_self_eq