English
Given a predicate p and two functions f,g with prescribed continuity on the respective sides of the frontier of p, the function a ↦ if p(a) then f(a) else g(a) is continuous on the domain where p is defined.
Русский
Дано предикат p и две функции f,g с заданной непрерывностью на соответствующих сторонах границы p; функция a ↦ if p(a) then f(a) else g(a) непрерывна на области определения.
LaTeX
$$$\text{ContinuousOn}\bigl(a\mapsto \text{ite}(p(a), f(a), g(a))\bigr)\text{ on the appropriate domain.}$$$
Lean4
theorem «if» {p : α → Prop} [∀ a, Decidable (p a)] (hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a)
(hf : ContinuousOn f <| s ∩ closure {a | p a}) (hg : ContinuousOn g <| s ∩ closure {a | ¬p a}) :
ContinuousOn (fun a => if p a then f a else g a) s :=
by
apply ContinuousOn.if'
· rintro a ha
simp only [← hp a ha, ite_self]
apply tendsto_nhdsWithin_mono_left (inter_subset_inter_right s subset_closure)
exact hf a ⟨ha.1, ha.2.1⟩
· rintro a ha
simp only [hp a ha, ite_self]
apply tendsto_nhdsWithin_mono_left (inter_subset_inter_right s subset_closure)
rcases ha with ⟨has, ⟨_, ha⟩⟩
rw [← mem_compl_iff, ← closure_compl] at ha
apply hg a ⟨has, ha⟩
· exact hf.mono (inter_subset_inter_right s subset_closure)
· exact hg.mono (inter_subset_inter_right s subset_closure)
