closure_singleton_eq_Iic

Mathlib.Topology.Inseparable

URI: https://scilib.ai/kg/mathlib#closure_singleton_eq_Iic

English

The closure of a singleton {x} is the set of all z with z ⤳ x.

Русский

Замыкание множества−одиночки {x} равно множеству всех z, таких что z ⤳ x.

LaTeX

$$$$ \overline{\{x\}} = \{ z:\; X \mid z \rightsquigarrow x \}. $$$$

Lean4

theorem closure_singleton_eq_Iic (x : X) : closure { x } = Iic x :=
  Set.ext fun _ ↦ specializes_iff_mem_closure.symm

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

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

Разделы

Аффилиация

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