card_eq_one

Mathlib.Data.Finset.Card

URI: https://scilib.ai/kg/mathlib#Finset.card_eq_one

English

A finite set has cardinality 1 exactly when it is a singleton.

Русский

Конченный набор имеет кардиналитет 1 тогда и только тогда, когда он одиночный.

LaTeX

$$$#s = 1 \\iff \\exists a, s = \\{ a \\}$$$

Lean4

theorem card_eq_one : #s = 1 ↔ ∃ a, s = { a } := by
  cases s
  simp only [Multiset.card_eq_one, Finset.card, ← val_inj, singleton_val]

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

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

Разделы

Аффилиация

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