mk_equiv_of_lift_eq — Mathlib

English

If lift(#α) = lift(#β'), then #(Equiv α β') = 2^{ lift(#α) }.

Русский

Если lift(#α) = lift(#β'), тогда #(Equiv α β') = 2^{ lift(#α) }.

LaTeX

$$$ (lift(#\\alpha) = lift(#\\beta')) \\implies #(α \\simeq β') = 2^{\\ lift(#\\alpha) } $$$

Lean4

theorem mk_equiv_of_lift_eq (leq : lift.{v} #α = lift.{u} #β') : #(α ≃ β') = 2 ^ lift.{v} #α := by
  erw [← (lift_mk_eq'.2 ⟨.equivCongr (.refl α) (lift_mk_eq'.1 leq).some⟩).trans (lift_id'.{u, v} _), lift_umax.{u, v},
    mk_perm_eq_two_power, lift_power, lift_natCast];
  rfl

Похожие утверждения