le_generateFrom

Mathlib.Topology.Order

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

← MathLib Explorer

English

If every s in g is open, then t ≤ generateFrom g.

Русский

Если каждый элемент семейства g открыт в топологии t, то t ⊆ generateFrom(g).

LaTeX

$$$\bigl( \forall s \in g,\ IsOpen(s) \bigr) \Rightarrow t \le \mathrm{generateFrom}(g)$$$

Lean4

theorem le_generateFrom {t : TopologicalSpace α} {g : Set (Set α)} (h : ∀ s ∈ g, IsOpen s) : t ≤ generateFrom g :=
  le_generateFrom_iff_subset_isOpen.2 h

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

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

Разделы

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

Аффилиация

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