mkD_of_continuousOn — Mathlib

English

Let s be a subset of X and assume f is continuous on s with f(0) = 0. Then mkD on the restricted function equals the pair built from the restriction and its continuity on s.

Русский

Пусть s ⊆ X, f непрерывна на s и f(0) = 0. Тогда mkD на ограниченной функции равняется паре, состоящей из ограниченной функции и её непрерывности на s, вместе с условием f(0) = 0.

LaTeX

$$mkD(s.restrict f) g = ⟨⟨s.restrict f, hf.restrict⟩, hf₀⟩$$

Lean4

theorem mkD_of_continuousOn {s : Set X} [Zero s] {f : X → R} {g : C(s, R)₀} (hf : ContinuousOn f s)
    (hf₀ : f (0 : s) = 0) : mkD (s.restrict f) g = ⟨⟨s.restrict f, hf.restrict⟩, hf₀⟩ :=
  mkD_of_continuous hf.restrict hf₀

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