topologicalSpace_eq_of_top — Mathlib

English

The topological space on the restricted product with principal filter equals the induced topology from the coe map.

Русский

Топология ограниченного произведения с principal-фильтром равна индуцированной топологии от отображения coe.

LaTeX

$$$\\topologicalSpace R A (\\mathcal P S) = \\text{induced}(\\operatorname{coe}, \\inferInstance)$ for principal S.$$

Lean4

theorem topologicalSpace_eq_of_top :
    topologicalSpace R A ⊤ = .induced ((↑) : Πʳ i, [R i, A i]_[⊤] → Π i, R i) inferInstance :=
  principal_univ ▸ topologicalSpace_eq_of_principal

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