Theorems · Theorem · Lie groups

RestrictedProduct.continuous_rng_of_principal

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

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace