sub_section — Mathlib

English

If s and t are ContMDiffOn on u, then s − t is ContMDiffOn on u.

Русский

Если s и t — ContMDiffOn на u, то s − t — ContMDiffOn на u.

LaTeX

$$ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x ((s - t) x)) u$$

Lean4

theorem sub_section (hs : ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) u)
    (ht : ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (t x)) u) :
    ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x ((s - t) x)) u := fun x₀ hx₀ ↦
  (hs x₀ hx₀).sub_section (ht x₀ hx₀)

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