Theorems · Theorem · general topology

continuous_pi

∀ {X : Type u} {ι : Type u_5} {A : ι → Type u_6} [inst : TopologicalSpace X] [T : (i : ι) → TopologicalSpace (A i)]
  {f : X → (i : ι) → A i}, (∀ (i : ι), Continuous fun a => f a i) → Continuous f

Defined in

Mathlib.Topology.Constructions

Cited by

43 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace