exists_ne

Mathlib.Data.Set.Subsingleton

URI: https://scilib.ai/kg/mathlib#Set.Nontrivial.exists_ne

← MathLib Explorer

English

For a nontrivial s, for any z there exists x ∈ s with x ≠ z.

Русский

Для подсинглотного s для любого z существует x ∈ s такой, что x ≠ z.

LaTeX

$$$ \forall z, (s.Nontrivial) \rightarrow \exists x \in s, x \neq z $$$

Lean4

theorem exists_ne (hs : s.Nontrivial) (z) : ∃ x ∈ s, x ≠ z :=
  by
  by_contra! H
  rcases hs with ⟨x, hx, y, hy, hxy⟩
  rw [H x hx, H y hy] at hxy
  exact hxy rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru