mfderivWithin_projIcc_one — Mathlib

English

The derivative of the projection onto Icc x y in the tangent space equals 1 at z with z ∈ Icc x y.

Русский

Производная проекции на Icc x y в касательном пространстве равна единице в точке z ∈ Icc x y.

LaTeX

$$$mfderivWithin 𝓘(ℝ) (\mathcal{R}∂ 1) (Set.projIcc x y h.out.le) (Icc x y) z 1 = 1$$$

Lean4

theorem mfderivWithin_projIcc_one {z : ℝ} (hz : z ∈ Icc x y) :
    mfderivWithin 𝓘(ℝ) (𝓡∂ 1) (Set.projIcc x y h.out.le) (Icc x y) z 1 = 1 :=
  by
  change _ = oneTangentSpaceIcc (Set.projIcc x y h.out.le z)
  simp only [oneTangentSpaceIcc]
  congr
  simp [projIcc_of_mem h.out.le hz]

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