continuous_if_const — Mathlib

English

If p is a proposition and Decidable, the function a ↦ if p then f a else g a is continuous whenever f and g are continuous (independently of p).

Русский

Если p — предложение и Decidable, функция a ↦ если p тогда f a иначе g a непрерывна, когда f и g непрерывны отдельно.

LaTeX

$$$\forall p,\ \text{Decidable } p\Rightarrow (\mathrm{Continuous}\ f \Rightarrow \mathrm{Continuous}\ g)\Rightarrow \mathrm{Continuous}\ (a\mapsto \mathrm{ite}(p, f(a), g(a))).$$$

Lean4

theorem continuous_if_const (p : Prop) [Decidable p] (hf : p → Continuous f) (hg : ¬p → Continuous g) :
    Continuous fun a => if p then f a else g a := by
  split_ifs with h
  exacts [hf h, hg h]

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