cardinalMk_eq

Mathlib.Algebra.FreeAlgebra.Cardinality

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

English

For empty X, the cardinality equals the cardinality of R.

Русский

Для пустого X мощность равна мощности R.

LaTeX

$$$[IsEmpty X] : \\#(FreeAlgebra R X) = \\#R$$$

Lean4

theorem cardinalMk_eq [IsEmpty X] : #(FreeAlgebra R X) = #R := by simp

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

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

Разделы

Аффилиация

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