card_le_one_iff_subsingleton

Mathlib.Data.Fintype.EquivFin

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

English

card α ≤ 1 is equivalent to α being subsingleton (any two elements are equal).

Русский

card α ≤ 1 эквивалентно тому, что α является одиночным (любые два элемента равны).

LaTeX

$$$\\operatorname{card} \\alpha \\le 1 \\iff \\operatorname{Subsingleton} \\alpha$$$

Lean4

theorem card_le_one_iff_subsingleton : card α ≤ 1 ↔ Subsingleton α :=
  card_le_one_iff.trans subsingleton_iff.symm

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

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

Разделы

Аффилиация

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