mono — Mathlib

English

If h is a derivative within t, and s ⊆ t, then h is also a derivative within s.

Русский

Если h — производная внутри t, и s ⊆ t, то h также производная внутри s.

LaTeX

$$h : HasMFDerivWithinAt I I' f t x f' → s ⊆ t → HasMFDerivWithinAt I I' f s x f'$$

Lean4

theorem mono (h : HasMFDerivWithinAt I I' f t x f') (hst : s ⊆ t) : HasMFDerivWithinAt I I' f s x f' :=
  ⟨ContinuousWithinAt.mono h.1 hst, HasFDerivWithinAt.mono h.2 (inter_subset_inter (preimage_mono hst) (Subset.refl _))⟩

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