Theorems · Theorem · general topology

Topology.ContinuousMapGeneratedBy.mk.injEq

∀ {ι : 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

0 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpace