exists_ne_of_one_lt_encard — Mathlib

English

If 1 < encard(s), then for every a in α there exists b in s with b ≠ a.

Русский

Если 1 < encard(S), то для любого a из типа найдется b ∈ S такой, что b ≠ a.

LaTeX

$$1 < encard(s) \\Rightarrow \\forall a, ∃ b ∈ s, b ≠ a$$

Lean4

theorem exists_ne_of_one_lt_encard (h : 1 < s.encard) (a : α) : ∃ b ∈ s, b ≠ a :=
  by
  by_contra! h'
  obtain ⟨b, b', hb, hb', hne⟩ := one_lt_encard_iff.1 h
  apply hne
  rw [h' b hb, h' b' hb']

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