exists_ne_of_one_lt_card — Mathlib

English

If 1 < card α and a ∈ α, then there exists b ∈ α with b ≠ a.

Русский

Если в α больше одного элемента и задана с ним пара, то существует другой элемент b ∈ α, отличный от a.

LaTeX

$$$(1 < \\operatorname{card} \\alpha) \\rightarrow (\\exists b: \\alpha, b \\neq a)$$$

Lean4

theorem exists_ne_of_one_lt_card (h : 1 < card α) (a : α) : ∃ b : α, b ≠ a :=
  haveI : Nontrivial α := one_lt_card_iff_nontrivial.1 h
  exists_ne a

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