mem_singleton

Mathlib.Topology.Sets.Closeds

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Closeds.mem_singleton

English

In a T1 space, an element a lies in the closed singleton {b} if and only if a = b.

Русский

В пространстве T1 элемент a принадлежит замкнутому множество {b} тогда и только тогда a = b.

LaTeX

$$[simp] theorem mem_singleton {a,b} : a ∈ singleton(b) ⇔ a = b.$$

Lean4

@[simp]
theorem mem_singleton [T1Space α] {a b : α} : a ∈ singleton b ↔ a = b :=
  Iff.rfl

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

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

Разделы

Аффилиация

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