mdifferentiable_of_mdifferentiableOn_iUnion_of_isOpen

English

If f is differentiable on two open patches s and t whose union is the whole space, then f is differentiable globally.

Русский

Если f дифференцируема на двух открытых участках s и t, чьё объединение покрывает всю пространство, то f дифференцируемо глобально.

LaTeX

$$$$MDifferentiableOn I I' f s \\rightarrow MDifferentiableOn I I' f t \\rightarrow s \\cup t = univ \\rightarrow IsOpen s \\rightarrow IsOpen t \\rightarrow MDifferentiable I I' f$$$$

Lean4

theorem mdifferentiable_of_mdifferentiableOn_iUnion_of_isOpen {ι : Type*} {s : ι → Set M}
    (hf : ∀ i : ι, MDifferentiableOn I I' f (s i)) (hs : ∀ i, IsOpen (s i)) (hs' : ⋃ i, s i = univ) :
    MDifferentiable I I' f := by
  rw [← mdifferentiableOn_univ, ← hs']
  exact MDifferentiableOn.iUnion_of_isOpen hf hs

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