two_le_iff — Mathlib

English

Two is less than or equal to the cardinality of α exactly when there exist two distinct elements in α.

Русский

Число 2 не превосходит кардинал множества α тогда, когда в α существуют два различных элемента.

LaTeX

$$$(2 : \\text{Cardinal}) \\le #\\alpha \\iff \\exists x,y : \\alpha, x \\neq y$$$

Lean4

theorem two_le_iff : (2 : Cardinal) ≤ #α ↔ ∃ x y : α, x ≠ y := by
  rw [← Nat.cast_two, nat_succ, succ_le_iff, Nat.cast_one, one_lt_iff_nontrivial, nontrivial_iff]

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