Theorems · Theorem · Lie groups

RestrictedProduct.continuous_dom

∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [inst : (i : ι) → TopologicalSpace (R i)]
  {X : Type u_3} [inst_1 : TopologicalSpace X] {f : RestrictedProduct (fun i => R i) (fun i => A i) 𝓕 → X},
  Continuous f ↔ ∀ (S : Set ι) (hS : 𝓕 ≤ Filter.principal S), Continuous (f ∘ RestrictedProduct.inclusion R A hS)

The universal property of the topology on the restricted product: a map from Πʳ i, [R i, A i]_[𝓕] is continuous iff its restriction to each Πʳ i, [R i, A i]_[𝓟 s] (with 𝓕 ≤ 𝓟 s) is continuous. See also RestrictedProduct.continuous_dom_prod_left.

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace