contMDiffOn_iUnion_iff_of_isOpen — Mathlib

English

For a map f on a subtype U ⊆ M, contMDiffAt on the inclusion corresponds to contMDiffAt on f on M.

Русский

Для отображения f на подтипе U ⊆ M, ContMDiffAt на включении эквивалентно ContMDiffAt на f на M.

LaTeX

$$ContMDiffAt_I_I'_n (f|_U) x ↔ ContMDiffAt_I_I'_n f x$$

Lean4

/-- A function is `C^k` on a union of open sets `s i` iff it is `C^k` on each `s i`. -/
theorem contMDiffOn_iUnion_iff_of_isOpen {ι : Type*} {s : ι → Set M} (hs : ∀ i, IsOpen (s i)) :
    ContMDiffOn I I' n f (⋃ i, s i) ↔ ∀ i : ι, ContMDiffOn I I' n f (s i) :=
  ⟨fun h i ↦ h.mono <| subset_iUnion_of_subset i fun _ a ↦ a, fun h ↦ ContMDiffOn.iUnion_of_isOpen h hs⟩

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