card_eq_two_iff — Mathlib

English

Nat.card α = 2 if and only if there exist two distinct elements x, y with {x, y} = univ.

Русский

Nat.card α = 2 тогда и только тогда, когда существуют два различных элемента x, y такие, что {x, y} = универсума.

LaTeX

$$$$ Nat.card(\alpha) = 2 \iff \exists x,y : \alpha, x \neq y \land \{x,y\} = \mathrm{univ}$$$$

Lean4

theorem card_eq_two_iff : Nat.card α = 2 ↔ ∃ x y : α, x ≠ y ∧ { x, y } = @Set.univ α :=
  toNat_eq_ofNat.trans mk_eq_two_iff

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