card_eq_two_iff'

Mathlib.SetTheory.Cardinal.Finite

URI: https://scilib.ai/kg/mathlib#Nat.card_eq_two_iff'

English

For a fixed x ∈ α, Nat.card α = 2 if and only if there exists a unique y ≠ x.

Русский

При фиксированном x ∈ α, Nat.card α = 2 тогда и только тогда, существует единственный y ≠ x.

LaTeX

$$$$ Nat.card(\alpha) = 2 \iff \exists! y, y \neq x $$$$

Lean4

theorem card_eq_two_iff' (x : α) : Nat.card α = 2 ↔ ∃! y, y ≠ x :=
  toNat_eq_ofNat.trans (mk_eq_two_iff' x)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru