card_constantsOn

Mathlib.ModelTheory.LanguageMap

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.card_constantsOn

English

The cardinality of the constants-on language on α equals the cardinality of α.

Русский

Кардинал языка констант на α равен кардиналу α.

LaTeX

$$$ (constantsOn \\alpha).card = #\\alpha $$$

Lean4

theorem card_constantsOn : (constantsOn α).card = #α := by
  simp [card_eq_card_functions_add_card_relations, sum_nat_eq_add_sum_succ]

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

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

Разделы

Аффилиация

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