card_eq_three — Mathlib

English

Let s be a finite set. Then |s| = 3 iff there exist pairwise distinct x, y, z with s = {x, y, z}.

Русский

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

LaTeX

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

Lean4

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

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