card_eq_one_of_forall_eq

Mathlib.Data.Fintype.EquivFin

URI: https://scilib.ai/kg/mathlib#Fintype.card_eq_one_of_forall_eq

English

If every element of α is equal to a fixed i, then card α = 1.

Русский

Если для фиксированного i каждый элемент α равен i, то card α = 1.

LaTeX

$$$(\\forall j: \\alpha, j = i) \\Rightarrow \\operatorname{card} \\alpha = 1$$$

Lean4

theorem card_eq_one_of_forall_eq {i : α} (h : ∀ j, j = i) : card α = 1 :=
  Fintype.card_eq_one_iff.2 ⟨i, h⟩

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

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

Разделы

Аффилиация

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