cardinalMk_eq_lift — Mathlib

English

If X is empty then the cardinality of FreeAlgebra R X equals lift(#R).

Русский

Если X пусто, то мощность FreeAlgebra R X равна lift(#R).

LaTeX

$$$\\text{IsEmpty }X \\Rightarrow \\#(FreeAlgebra R X) = \\operatorname{lift}(\\#R)$$$

Lean4

@[simp]
theorem cardinalMk_eq_lift [IsEmpty X] : #(FreeAlgebra R X) = Cardinal.lift.{v} #R :=
  by
  have := lift_mk_eq'.2 ⟨show (FreeMonoid X →₀ R) ≃ R from Equiv.finsuppUnique⟩
  rw [lift_id'.{u, v}, lift_umax] at this
  rwa [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra]

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