if_const — Mathlib

English

If f is continuous on closure of s and g is continuous on closure of the complement of s, then the piecewise function piecewise s f g is continuous on the whole space.

Русский

Если f непрерывна на замкнутой окрестности s, а g — на замкнутой окрестности дополнения s, тогда piecewise s f g непрерывна во всём пространстве.

LaTeX

$$$\text{Continuous}(\mathrm{piecewise}\ s\ f\ g).$$$

Lean4

theorem if_const (p : Prop) [Decidable p] (hf : Continuous f) (hg : Continuous g) :
    Continuous fun a => if p then f a else g a :=
  continuous_if_const p (fun _ => hf) fun _ => hg

Похожие утверждения