mfderiv_subtype_coe_Icc_one — Mathlib

English

For z ∈ Icc x y, the mfderiv ofSubtype.val equals 1 in the tangent space.

Русский

Для z ∈ Icc x y производная mfderiv подтиповой карты равна единице.

LaTeX

$$$mfderiv (\mathcal{R}∂ 1) 𝓘(ℝ) (Subtype.val : Icc x y → ℝ) z 1 = 1$$$

Lean4

theorem mfderiv_subtype_coe_Icc_one (z : Icc x y) : mfderiv (𝓡∂ 1) 𝓘(ℝ) (Subtype.val : Icc x y → ℝ) z 1 = 1 :=
  by
  have A :
    mfderivWithin 𝓘(ℝ) 𝓘(ℝ) (Subtype.val ∘ (projIcc x y h.out.le)) (Icc x y) z 1 =
      mfderivWithin 𝓘(ℝ) 𝓘(ℝ) id (Icc x y) z 1 :=
    by
    congr 1
    apply mfderivWithin_congr_of_mem _ z.2
    intro z hz
    simp [projIcc_of_mem h.out.le hz]
  rw [← mfderivWithin_comp_projIcc_one, A]
  simp only [id_eq, mfderivWithin_eq_fderivWithin]
  rw [fderivWithin_id (uniqueDiffOn_Icc h.out _ z.2)]
  rfl

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