cardinalMk_eq_max

Mathlib.Algebra.FreeAlgebra.Cardinality

URI: https://scilib.ai/kg/mathlib#FreeAlgebra.cardinalMk_eq_max

English

If X is nonempty and R is nontrivial then the cardinality is the max of #R, #X, and ℵ0.

Русский

Если X непусто и R ненулевой, мощность равна максимуму #R, #X и ℵ0.

LaTeX

$$$[Nonempty X] [Nontrivial R] : \\#(FreeAlgebra R X) = #R \\sqcup #X \\sqcup \\aleph_0$$$

Lean4

theorem cardinalMk_eq_max [Nonempty X] [Nontrivial R] : #(FreeAlgebra R X) = #R ⊔ #X ⊔ ℵ₀ := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru