encard_le_one_iff — Mathlib

English

encard(s) ≤ 1 if and only if s is subsingleton.

Русский

encard(S) ≤ 1 если и только если S является подвселенной.

LaTeX

$$$encard(s) \\le 1 \\iff s.Subsingleton$$$

Lean4

theorem encard_le_one_iff : s.encard ≤ 1 ↔ ∀ a b, a ∈ s → b ∈ s → a = b :=
  by
  rw [encard_le_one_iff_eq, or_iff_not_imp_left, ← Ne, ← nonempty_iff_ne_empty]
  refine ⟨fun h a b has hbs ↦ ?_, fun h ⟨x, hx⟩ ↦ ⟨x, ((singleton_subset_iff.2 hx).antisymm' (fun y hy ↦ h _ _ hy hx))⟩⟩
  obtain ⟨x, rfl⟩ := h ⟨_, has⟩
  rw [(has : a = x), (hbs : b = x)]

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