mono — Mathlib

English

If ContMDiffWithinAt holds on a set s, and s and t agree near x (nhds), then ContMDiffWithinAt also holds on t at x.

Русский

Если ContMDiffWithinAt справедлив для множества s, и s и t совпадают в окрестности x, тогда ContMDiffWithinAt выполняется и на t в x.

LaTeX

$$$ ContMDiffWithinAt I I' n f s x \rightarrow (s =_{nhds x} t) \Rightarrow ContMDiffWithinAt I I' n f t x $$$

Lean4

theorem mono (hf : ContMDiffWithinAt I I' n f s x) (hts : t ⊆ s) : ContMDiffWithinAt I I' n f t x :=
  hf.mono_of_mem_nhdsWithin <| mem_of_superset self_mem_nhdsWithin hts

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