exists_ne_of_one_lt_ncard — Mathlib

English

Let s be a subset of a type α with more than one element. Then for every a, there exists b ∈ s with b ≠ a.

Русский

Пусть s — подмножество типа α с более чем одним элементом. Тогда для каждого a найдется b ∈ s такой, что b ≠ a.

LaTeX

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

Lean4

theorem exists_ne_of_one_lt_ncard (hs : 1 < s.ncard) (a : α) : ∃ b, b ∈ s ∧ b ≠ a :=
  by
  have hsf := finite_of_ncard_ne_zero (zero_lt_one.trans hs).ne.symm
  rw [ncard_eq_toFinset_card _ hsf] at hs
  simpa only [Finite.mem_toFinset] using Finset.exists_mem_ne hs a

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