cardinalMk_le_max

Mathlib.Algebra.FreeAlgebra.Cardinality

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

English

The cardinality is bounded above by the max of R, X, and ℵ0.

Русский

Мощность ограничена сверху максимумом мощности R, X и ℵ0.

LaTeX

$$$\\#(FreeAlgebra R X) \\le #R \\sqcup #X \\sqcup \\aleph_0$$$

Lean4

theorem cardinalMk_le_max : #(FreeAlgebra R X) ≤ #R ⊔ #X ⊔ ℵ₀ := by simpa using cardinalMk_le_max_lift R X

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

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

Разделы

Аффилиация

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