isOpen_generateFrom_of_mem

Mathlib.Topology.Order

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.isOpen_generateFrom_of_mem

English

If s ∈ g, then s is open in the topology generated by g.

Русский

Если s принадлежит g, то s открыто в топологии, порождённой g.

LaTeX

$$$s \\in g \\Rightarrow s \\text{ is open in generateFrom}(g).$$$

Lean4

theorem isOpen_generateFrom_of_mem {g : Set (Set α)} {s : Set α} (hs : s ∈ g) : IsOpen[generateFrom g] s :=
  GenerateOpen.basic s hs

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

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

Разделы

Аффилиация

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