subsingleton_iff_singleton

Mathlib.Data.Set.Subsingleton

URI: https://scilib.ai/kg/mathlib#Set.subsingleton_iff_singleton

← MathLib Explorer

English

If x ∈ s, then s.Subsingleton ↔ s = {x}.

Русский

Если x ∈ s, то s.Subsingleton эквивалентно s = {x}.

LaTeX

$$$ s.Subsingleton \;\iff\; s = { x } $$$

Lean4

theorem subsingleton_iff_singleton {x} (hx : x ∈ s) : s.Subsingleton ↔ s = { x } :=
  ⟨fun h => h.eq_singleton_of_mem hx, fun h => h.symm ▸ subsingleton_singleton⟩

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

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

Разделы

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

Аффилиация

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