ncard_eq_four — Mathlib

English

A set s has cardinality 4 iff there exist pairwise distinct x, y, z, w with s = {x, y, z, w}.

Русский

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

LaTeX

$$$s.ncard = 4 \iff \exists x \exists y \exists z \exists w\ (\text{pairwise distinct}) \land s = \{x,y,z,w\}$$$

Lean4

theorem ncard_eq_four : s.ncard = 4 ↔ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = { x, y, z, w } :=
  by
  rw [← encard_eq_four, ncard_def]
  simp

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