ncard_eq_three — Mathlib

English

A set s has cardinality 3 if and only if there exist pairwise distinct x, y, z with s = {x, y, z}.

Русский

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

LaTeX

$$$s.ncard = 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 ncard_eq_three : s.ncard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = { x, y, z } :=
  by
  rw [← encard_eq_three, ncard_def]
  simp

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