English
If each s_i is open, ContMDiffOn on the union is equivalent to ContMDiffOn on all pieces.
Русский
Если каждое множество s_i открыто, то ContMDiffOn на объединении эквивалентно ContMDiffOn на каждой части.
LaTeX
$$$\forall i,\ IsOpen(s_i) \Rightarrow ContMDiffOn I I' n f (\bigcup_i s_i) \Leftrightarrow \forall i, ContMDiffOn I I' n f (s_i)$$$
Lean4
/-- If a function is `C^k` on two open sets, it is also `C^n` on their union. -/
theorem union_of_isOpen (hf : ContMDiffOn I I' n f s) (hf' : ContMDiffOn I I' n f t) (hs : IsOpen s) (ht : IsOpen t) :
ContMDiffOn I I' n f (s ∪ t) := by
intro x hx
obtain (hx | hx) := hx
· exact (hf x hx).contMDiffAt (hs.mem_nhds hx) |>.contMDiffWithinAt
· exact (hf' x hx).contMDiffAt (ht.mem_nhds hx) |>.contMDiffWithinAt
