Theorems · Inductive type · general topology

Topology.ContinuousMapGeneratedBy

{ι : Type t} →
  (X : ι → Type u) →
    [(i : ι) → TopologicalSpace (X i)] →
      (Y : Type v) → [TopologicalSpace Y] → (Z : Type v') → [TopologicalSpace Z] → Type (max v v')

The (bundled) type of X-continuous maps Y → Z.

Defined in

Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Cited by

28 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpace