eq_singleton_of_mem

Mathlib.Data.Set.Subsingleton

URI: https://scilib.ai/kg/mathlib#Set.Subsingleton.eq_singleton_of_mem

← MathLib Explorer

English

If s is subsingleton and x ∈ s, then s = {x}.

Русский

Если s субоднозначно и x ∈ s, то s = {x}.

LaTeX

$$$ hs : s.Subsingleton \; \to \; hx : x \in s \Rightarrow s = { x } $$$

Lean4

theorem eq_singleton_of_mem (hs : s.Subsingleton) {x : α} (hx : x ∈ s) : s = { x } :=
  ext fun _ => ⟨fun hy => hs hx hy ▸ mem_singleton _, fun hy => (eq_of_mem_singleton hy).symm ▸ hx⟩

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

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

Разделы

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

Аффилиация

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