ncard_le_one_iff_subsingleton

Mathlib.Data.Set.Card

URI: https://scilib.ai/kg/mathlib#Set.ncard_le_one_iff_subsingleton

English

For finite s, s.ncard ≤ 1 holds if and only if s is subsingleton.

Русский

Для конечного s выполняется s.ncard ≤ 1 ⇔ s является подсинглтонным множеством.

LaTeX

$$$$ \text{[Finite } s] \; s.ncard \le 1 \iff s.Subsingleton $$$$

Lean4

@[simp]
theorem ncard_le_one_iff_subsingleton [Finite s] : s.ncard ≤ 1 ↔ s.Subsingleton :=
  ncard_le_one <| inferInstanceAs (Finite s)

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

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

Разделы

Аффилиация

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