Theorems · Theorem · general topology

Topology.ContinuousMapGeneratedBy.continuousGeneratedBy_iff_uncurry

∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y]
  {Z : Type v'} [inst_2 : TopologicalSpace Z] {T : Type v''} [inst_3 : TopologicalSpace T]
  [∀ (i : ι), LocallyCompactSpace (X i)] (g : Z → Topology.ContinuousMapGeneratedBy X Y T),
  Topology.ContinuousGeneratedBy X g ↔
    ∀ ⦃i₁ : ι⦄ (f₁ : C(X i₁, Z)) ⦃i₂ : ι⦄ (f₂ : C(X i₂, Y)),
      Continuous fun x =>
        match x with
        | (x₁, x₂) => (g (f₁ x₁)) (f₂ x₂)

Defined in

Mathlib.Topology.Convenient.HomSpace

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceLocallyCompactSpace