English
If f', g' are continuous and the same patching hypotheses hold as in the previous result, then the piecewise-defined map x ↦ if f(x) ≤ g(x) then f'(x) else g'(x) is continuous.
Русский
Если f', g' непрерывны и выполняются такие же условия стыковки, как в предыдущем результате, то отображение x ↦ если f(x) ≤ g(x) то f'(x) иначе g'(x) непрерывно.
LaTeX
$$$\Big( (hf': Continuous f') \land (hg': Continuous g') \land (hf: Continuous f) \land (hg: Continuous g) \land (\forall x, f(x) = g(x) \Rightarrow f'(x) = g'(x)) \Big) \Rightarrow \\quad \text{Continuous}\Bigl(x \mapsto \begin{cases} f'(x) & f(x) \le g(x) \\ g'(x) & \text{otherwise} \end{cases}\Bigr).$$$
Lean4
theorem if_le [TopologicalSpace γ] [∀ x, Decidable (f x ≤ g x)] {f' g' : β → γ} (hf' : Continuous f')
(hg' : Continuous g') (hf : Continuous f) (hg : Continuous g) (hfg : ∀ x, f x = g x → f' x = g' x) :
Continuous fun x => if f x ≤ g x then f' x else g' x :=
continuous_if_le hf hg hf'.continuousOn hg'.continuousOn hfg
