mkD_eq_mkD_of_map_zero — Mathlib

English

If f(0) = 0, then mkD f g is equal to the standard mkD constructed via the map f into R.

Русский

При условии f(0) = 0, mkD f g равен стандартной конструкции mkD через отображение f в R.

LaTeX

$$mkD f g = ContinuousMap.mkD f g$$

Lean4

/-- Link between `ContinuousMapZero.mkD` and `ContinuousMap.mkD`. -/
theorem mkD_eq_mkD_of_map_zero [Zero X] (f : X → R) (g : C(X, R)₀) (f_zero : f 0 = 0) :
    mkD f g = ContinuousMap.mkD f g := by
  ext
  by_cases f_cont : Continuous f <;>
    simp [*, ContinuousMap.mkD_of_continuous, mkD_of_continuous, mkD_of_not_continuous,
      ContinuousMap.mkD_of_not_continuous]

Похожие утверждения