mk_equiv_eq_arrow_of_lift_eq — Mathlib

English

For infinite α, β' and any lift equality leq between lift(#α) and lift(#β'), then #(Equiv α β') = 2^{lift(#α)}.

Русский

Для бесконечных α, β' и при равенстве подъёмов между lift(#α) и lift(#β'), число эквивалентностей равно 2^{lift(#α)}.

LaTeX

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

Lean4

theorem mk_equiv_eq_arrow_of_lift_eq (leq : lift.{v} #α = lift.{u} #β') : #(α ≃ β') = #(α → β') :=
  by
  obtain ⟨e⟩ := lift_mk_eq'.mp leq
  have e₁ := lift_mk_eq'.mpr ⟨.equivCongr (.refl α) e⟩
  have e₂ := lift_mk_eq'.mpr ⟨.arrowCongr (.refl α) e⟩
  rw [lift_id'.{u, v}] at e₁ e₂
  rw [← e₁, ← e₂, lift_inj, mk_perm_eq_self_power, power_def]

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