mono — Mathlib

English

If MDifferentiableWithinAt holds on a larger set t, then it holds on any smaller s ⊆ t.

Русский

Если MDifferentiableWithinAt верно на большем множестве t, то верно и на любом подмножестве s ⊆ t.

LaTeX

$$MDifferentiableWithinAt I I' f t x → s ⊆ t → MDifferentiableWithinAt I I' f s x$$

Lean4

theorem mono (hst : s ⊆ t) (h : MDifferentiableWithinAt I I' f t x) : MDifferentiableWithinAt I I' f s x :=
  ⟨ContinuousWithinAt.mono h.1 hst,
    DifferentiableWithinAt.mono h.differentiableWithinAt_writtenInExtChartAt
      (inter_subset_inter_left _ (preimage_mono hst))⟩

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