Theorems · Theorem · general topology

Topology.WithGeneratedByTopology.continuous_from_iff

∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  {Z : Type v'} [inst_1 : TopologicalSpace Z] (g : Topology.WithGeneratedByTopology X Y → Z),
  Continuous g ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous (g ∘ ⇑Topology.WithGeneratedByTopology.equiv.symm ∘ ⇑f)

Defined in

Mathlib.Topology.Convenient.GeneratedBy

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpace