cardinalMk_le_max_lift — Mathlib

English

The cardinality of FreeAlgebra R X does not exceed the maximum of lift(#R), lift(#X), and aleph0.

Русский

Мощность FreeAlgebra R X не превышает максимум среди lift(#R), lift(#X) и ℵ0.

LaTeX

$$$\\#(FreeAlgebra R X) \\le \\operatorname{lift}.{v} (\\#R) \\sqcup \\operatorname{lift}.{u} (\\#X) \\sqcup \\aleph_0$$$

Lean4

theorem cardinalMk_le_max_lift : #(FreeAlgebra R X) ≤ Cardinal.lift.{v} #R ⊔ Cardinal.lift.{u} #X ⊔ ℵ₀ :=
  by
  cases subsingleton_or_nontrivial R
  · exact (cardinalMk_eq_one R X).trans_le (le_max_of_le_right one_le_aleph0)
  cases isEmpty_or_nonempty X
  · exact (cardinalMk_eq_lift R X).trans_le (le_max_of_le_left <| le_max_left _ _)
  · exact (cardinalMk_eq_max_lift R X).le

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