generateFrom_inter — Mathlib

English

For a and b topologies on α, the topology generated by the intersection of their open sets equals the supremum a ⊔ b.

Русский

Для топологий a и b на α порождаемая топология из пересечения их открытых множеств равна объединению a ⊔ b.

LaTeX

$$$\\operatorname{generateFrom}\\bigl(\\{s \\mid \\mathrm{IsOpen}[a]\,s\\} \\cap \\{s \\mid \\mathrm{IsOpen}[b]\,s\\}\\bigr) = a \\sqcup b$$$

Lean4

theorem generateFrom_inter (a b : TopologicalSpace α) : generateFrom ({s | IsOpen[a] s} ∩ {s | IsOpen[b] s}) = a ⊔ b :=
  (gciGenerateFrom α).u_sup_l _ _

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