generateFrom_union_isOpen — Mathlib

English

For topologies a and b on α, the generatedFrom of the union of their open sets equals the infimum a ⊓ b.

Русский

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

LaTeX

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

Lean4

theorem generateFrom_union_isOpen (a b : TopologicalSpace α) :
    generateFrom ({s | IsOpen[a] s} ∪ {s | IsOpen[b] s}) = a ⊓ b :=
  (gciGenerateFrom α).u_inf_l _ _

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