English
Let p be a predicate on α, and f,g functions with appropriate continuity on the regions where p holds and does not hold, together with compatibility conditions along the boundary defined by frontier p. Then the function a ↦ if p(a) then f(a) else g(a) is continuous on the set s.
Русский
Пусть p — предикат на пространстве α, и функции f,g имеют соответствующую непрерывность на областях, где p(a) выполняется, и где не выполняется, вместе с условиями совместимости на границе, заданной frontier p. Тогда функция a ↦ если p(a) тогда f(a) иначе g(a) непрерывна на множестве s.
LaTeX
$$$\forall a\in s,\; \text{ContinuousOn}\bigl(a\mapsto \operatorname{ite}(p(a), f(a), g(a))\bigr)\; \text{on } s$ (under the stated boundary and continuity hypotheses).$$
Lean4
theorem if' {s : Set α} {p : α → Prop} {f g : α → β} [∀ a, Decidable (p a)]
(hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 <| if p a then f a else g a))
(hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 <| if p a then f a else g a))
(hf : ContinuousOn f <| s ∩ {a | p a}) (hg : ContinuousOn g <| s ∩ {a | ¬p a}) :
ContinuousOn (fun a => if p a then f a else g a) s :=
by
intro x hx
by_cases hx' : x ∈ frontier {a | p a}
· exact (hpf x ⟨hx, hx'⟩).piecewise_nhdsWithin (hpg x ⟨hx, hx'⟩)
· rw [← inter_univ s, ← union_compl_self {a | p a}, inter_union_distrib_left] at hx ⊢
rcases hx with hx | hx
· apply ContinuousWithinAt.union
· exact (hf x hx).congr (fun y hy => if_pos hy.2) (if_pos hx.2)
· have : x ∉ closure {a | p a}ᶜ := fun h => hx' ⟨subset_closure hx.2, by rwa [closure_compl] at h⟩
exact continuousWithinAt_of_notMem_closure fun h => this (closure_inter_subset_inter_closure _ _ h).2
· apply ContinuousWithinAt.union
· have : x ∉ closure {a | p a} := fun h => hx' ⟨h, fun h' : x ∈ interior {a | p a} => hx.2 (interior_subset h')⟩
exact continuousWithinAt_of_notMem_closure fun h => this (closure_inter_subset_inter_closure _ _ h).2
· exact (hg x hx).congr (fun y hy => if_neg hy.2) (if_neg hx.2)
