Theorems · Inductive type · functional analysis

ContinuousMapZero

(X : Type u_1) → (R : Type u_2) → [Zero X] → [Zero R] → [TopologicalSpace X] → [TopologicalSpace R] → Type (max u_1 u_2)

The type of continuous maps which map zero to zero. Note that one should never use the structure projection ContinuousMapZero.toContinuousMap and instead favor the coercion (↑) : C(X, R)₀ → C(X, R) available from the instance of ContinuousMapClass. All the instances on C(X, R)₀ from C(X, R) passes through this coercion, not the structure projection. Of course, the two are definitionally equal, but not reducibly so.

Defined in

Mathlib.Topology.ContinuousMap.ContinuousMapZero

Cited by

167 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

ZeroZeroTopologicalSpaceTopologicalSpace