card_eq_two — Mathlib

English

Let s be a finite set. Then |s| = 2 if and only if there exist distinct x and y with s = {x, y}.

Русский

Пусть s — конечное множество. Тогда |s| = 2 эквивалентно существованию попарно различных x и y таких, что s = {x, y}.

LaTeX

$$$|s| = 2 \\iff \\exists x \\exists y\\,(x \\neq y) \\land s = \\{ x, y \\}$$$

Lean4

theorem card_eq_two : #s = 2 ↔ ∃ x y, x ≠ y ∧ s = { x, y } :=
  by
  constructor
  · rw [card_eq_succ]
    grind [card_eq_one]
  · grind

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