Theorems · Theorem · general topology

ContinuousMap.mk.congr_simp

∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (toFun toFun_1 : X → Y)
  (e_toFun : toFun = toFun_1) (continuous_toFun : Continuous toFun),
  { toFun := toFun, continuous_toFun := continuous_toFun } = { toFun := toFun_1, continuous_toFun := ⋯ }

Defined in

Mathlib.Topology.ContinuousMap.Basic

Cited by

18 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpace