English
Let α be a linearly ordered topological space with an order-closed topology. For β → α and γ-valued outputs, consider f, g : β → α and f', g' : β → γ. If f and g are continuous, f' is continuous on {x | f(x) ≤ g(x)} and g' is continuous on {x | g(x) ≤ f(x)}, and if f(x) = g(x) implies f'(x) = g'(x) for all x, then the function x ↦ if f(x) ≤ g(x) then f'(x) else g'(x) is continuous.
Русский
Пусть α — линейно упорядоченное топологическое пространство сOrder-Closed topology. Пусть β, γ — топологические множества. Рассмотрим функции f, g : β → α и f', g' : β → γ. Предположим, что f и g непрерывны, f' непрерывна на области {x | f(x) ≤ g(x)}, a g' непрерывна на {x | g(x) ≤ f(x)}, и для всех x выполнено f(x) = g(x) ⇒ f'(x) = g'(x). Тогда функция x ↦ если f(x) ≤ g(x) то f'(x) иначе g'(x) является непрерывной.
LaTeX
$$$\Big( (hf: Continuous f) \land (hg: Continuous g) \land (hf': ContinuousOn f'\{x \mid f(x) \le g(x)\}) \land (hg': ContinuousOn g'\{x \mid g(x) \le f(x)\}) \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 continuous_if_le [TopologicalSpace γ] [∀ x, Decidable (f x ≤ g x)] {f' g' : β → γ} (hf : Continuous f)
(hg : Continuous g) (hf' : ContinuousOn f' {x | f x ≤ g x}) (hg' : ContinuousOn g' {x | g x ≤ f x})
(hfg : ∀ x, f x = g x → f' x = g' x) : Continuous fun x => if f x ≤ g x then f' x else g' x :=
by
refine continuous_if (fun a ha => hfg _ (frontier_le_subset_eq hf hg ha)) ?_ (hg'.mono ?_)
· rwa [(isClosed_le hf hg).closure_eq]
· simp only [not_le]
exact closure_lt_subset_le hg hf
