English
For any predicate p with decidable truth, if f and g satisfy specified limiting behavior along the frontier of p, then the function a ↦ if p(a) then f(a) else g(a) is continuous on the entire domain.
Русский
Для любого предиката p с разрешимой истиной, если f и g удовлетворяют заданному предельному поведению вдоль границы p, то функция a ↦ если p(a) тогда f(a) иначе g(a) непрерывна на всей области.
LaTeX
$$$\text{ContinuousOn}\;f\((\text{domain of } p) \) \to \text{ContinuousOn}\;g\rightarrow \text{Continuous}\;\lambda a. \mathbf{1}_{p(a)} f(a) + \mathbf{1}_{\neg p(a)} g(a).$$$
Lean4
theorem continuous_if' {p : α → Prop} [∀ a, Decidable (p a)]
(hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 <| ite (p a) (f a) (g a)))
(hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 <| ite (p a) (f a) (g a)))
(hf : ContinuousOn f {x | p x}) (hg : ContinuousOn g {x | ¬p x}) : Continuous fun a => ite (p a) (f a) (g a) :=
by
rw [← continuousOn_univ]
apply ContinuousOn.if' <;> simp [*] <;> assumption
