Theorems · Theorem · general topology

Topology.ContinuousMapGeneratedBy.mk.inj

∀ {ι : Type t} {X : ι → Type u} {inst : (i : ι) → TopologicalSpace (X i)} {Y : Type v} {inst_1 : TopologicalSpace Y}
  {Z : Type v'} {inst_2 : TopologicalSpace Z} {toFun : Y → Z} {prop : Topology.ContinuousGeneratedBy X toFun}
  {toFun_1 : Y → Z} {prop_1 : Topology.ContinuousGeneratedBy X toFun_1},
  { toFun := toFun, prop := prop } = { toFun := toFun_1, prop := prop_1 } → toFun = toFun_1

Defined in

Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Cited by

1 results in Mathlib

Foundations

Depth 21 from the axioms · uses no axioms