Theorems · Theorem · general topology

Topology.ContinuousMapGeneratedBy.curryEquiv_symm_apply

∀ {ι : 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]
  [inst_4 : ∀ (i : ι), LocallyCompactSpace (X i)] [inst_5 : ∀ (i j : ι), Topology.IsGeneratedBy X (X i × X j)]
  (g : Topology.ContinuousMapGeneratedBy X Z (Topology.ContinuousMapGeneratedBy X Y T)) (y : Y) (z : Z),
  (Topology.ContinuousMapGeneratedBy.curryEquiv.symm g) (y, z) = (g z) y

Defined in

Mathlib.Topology.Convenient.HomSpace

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceLocallyCompactSpaceTopology.IsGeneratedBy