min — Mathlib

English

The minimum of two continuous functions is continuous.

Русский

Минимум двух непрерывных функций — непрерывна.

LaTeX

$$$\text{Continuous }f \land \text{Continuous }g \Rightarrow \text{Continuous}(x \mapsto \min\{f(x), g(x)\}).$$$

Lean4

@[continuity, fun_prop]
protected theorem min (hf : Continuous f) (hg : Continuous g) : Continuous fun b => min (f b) (g b) :=
  by
  simp only [min_def]
  exact hf.if_le hg hf hg fun x => id

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