card_le_one_iff — Mathlib

English

If s is a finite set, then |s| ≤ 1 iff s is a singleton; equivalently, there exists a y such that s ⊆ {y}.

Русский

Если s — конечное множество, то |s| ≤ 1 эквивалентно тому, что s — синглтон, эквивалентно существованию y с s ⊆ {y}.

LaTeX

$$$#s \\le 1 \\iff \\exists y, s \\subseteq {y}$$$

Lean4

theorem card_le_one_iff : #s ≤ 1 ↔ ∀ {a b}, a ∈ s → b ∈ s → a = b := by grind [card_le_one]

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