cardinalMk_eq_max_lift — Mathlib

English

The cardinality of FreeAlgebra R X equals lift(#R) ⊔ lift(#X) ⊔ ℵ0, under standard nonemptiness and nontriviality assumptions.

Русский

Мощность множества FreeAlgebra R X равна lift(#R) ⊔ lift(#X) ⊔ ℵ0 при стандартных предположениях о непустоте и ненулевости.

LaTeX

$$$\\#(FreeAlgebra R X) = \\operatorname{lift}(\\#R) \\sqcup \\operatorname{lift}(\\#X) \\sqcup \\aleph_0$$$

Lean4

@[simp]
theorem cardinalMk_eq_max_lift [Nonempty X] [Nontrivial R] :
    #(FreeAlgebra R X) = Cardinal.lift.{v} #R ⊔ Cardinal.lift.{u} #X ⊔ ℵ₀ :=
  by
  have hX := mk_freeMonoid X
  rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra, mk_finsupp_lift_of_infinite, hX, lift_max,
    lift_aleph0, sup_comm, ← sup_assoc]

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