English
The topology on the restricted product is the supremum (iSup) of principal-coinduced topologies coming from all principal inclusions; formally, topologicalSpace R A 𝓕 equals the supremum of coinduced topologies along inclusions for all S with 𝓕 ≤ 𝓟 S.
Русский
Топология ограниченного произведения есть верхняя грань по отношению коиндукции над топологиями, получаемыми из всех инклюзий по принципу; формально, топология равна верхней границе по включениям для всех S с 𝓕 ≤ 𝓟 S.
LaTeX
$$$\\text{topologicalSpace } R A 𝓕 = \\bigvee_{S} \\big( \\text{TopologicalSpace.coinduced} (\\text{RestrictedProduct.inclusion } R A hS) (\\text{RestrictedProduct.topologicalSpace } R A (𝓟 S))\\bigr)$$$
Lean4
theorem topologicalSpace_eq_iSup :
topologicalSpace R A 𝓕 = ⨆ (S : Set ι) (hS : 𝓕 ≤ 𝓟 S), .coinduced (inclusion R A hS) (topologicalSpace R A (𝓟 S)) :=
by simp_rw [topologicalSpace_eq_of_principal, topologicalSpace]
