card_le_one — Mathlib

English

For any finite s, #s ≤ 1 is equivalent to the property that any two elements of s are equal (subsingleton).

Русский

Для любого конечного s условие |s| ≤ 1 эквивалентно свойству, что любые два элемента s равны (подмножество).

LaTeX

$$$#s \\le 1 \\iff \\forall a,b \\in s, a = b$$$

Lean4

theorem card_le_one : #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b :=
  by
  obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
  · simp
  refine (Nat.succ_le_of_lt (card_pos.2 ⟨x, hx⟩)).ge_iff_eq'.trans (card_eq_one.trans ⟨?_, ?_⟩)
  · grind
  · exact fun h => ⟨x, by grind⟩

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