Theorems · Theorem · Lie groups

RestrictedProduct.topologicalSpace_eq_iSup

∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} (𝓕 : Filter ι) [inst : (i : ι) → TopologicalSpace (R i)],
  RestrictedProduct.topologicalSpace R A 𝓕 =
    ⨆ S,
      ⨆ (hS : 𝓕 ≤ Filter.principal S),
        TopologicalSpace.coinduced (RestrictedProduct.inclusion R A hS)
          (RestrictedProduct.topologicalSpace R A (Filter.principal S))

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Cited by

2 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace