Theorems · Theorem · Lie groups

RestrictedProduct.continuous_dom_prod_right

∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  (∀ (i : ι), IsOpen (A i)) →
    ∀ {X : Type u_3} {Y : Type u_4} [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace Y]
      {f : RestrictedProduct (fun i => R i) (fun i => A i) Filter.cofinite × Y → X},
      Continuous f ↔
        ∀ (S : Set ι) (hS : Filter.cofinite ≤ Filter.principal S),
          Continuous (f ∘ Prod.map (RestrictedProduct.inclusion R A hS) id)

The universal property with parameters of the topology on the restricted product: for any topological space Y of "parameters", a map from (Πʳ i, [R i, A i]) × Y is continuous iff its restriction to each (Πʳ i, [R i, A i]_[𝓟 S]) × Y (with S cofinite) is continuous.

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpace