exists_mem_ne — Mathlib

English

If the cardinality of s is greater than 1, then for any a there exists b in s such that b ≠ a.

Русский

Если кардиналитет s больше единицы, то для любого элемента a существует b в s такой, что b ≠ a.

LaTeX

$$$1 < |s| \\Rightarrow \\forall a, \\exists b \\in s, b \\neq a$$$

Lean4

theorem exists_mem_ne (hs : 1 < #s) (a : α) : ∃ b ∈ s, b ≠ a :=
  by
  have : Nonempty α := ⟨a⟩
  by_contra!
  exact hs.not_ge (card_le_one_iff_subset_singleton.2 ⟨a, subset_singleton_iff'.2 this⟩)

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