contMDiffOn_iff_contDiffOn — Mathlib

English

The global ContMDiffOn between two model-with-corners spaces on a subset s is equivalent to ContDiffOn on s.

Русский

Глобальная ContMDiffOn между двумя моделями с углами на подмножестве s равносильна ContDiffOn на s.

LaTeX

$$$\ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s \iff \ContDiffOn 𝕜 n f s$$$

Lean4

theorem contMDiffOn_iff_contDiffOn {f : E → E'} {s : Set E} : ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E') n f s ↔ ContDiffOn 𝕜 n f s :=
  forall_congr' <| by simp [contMDiffWithinAt_iff_contDiffWithinAt]

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