sup — Mathlib

English

The pointwise maximum of two continuous functions into a lattice with ContinuousSup is continuous.

Русский

Пусть две непрерывные функции в решетке сходятся; максимум по каждому аргументу непрерывен.

LaTeX

$$$\\text{Continuous}(f) \\land \\text{Continuous}(g) \\Rightarrow \\text{Continuous}(x \\mapsto f(x) \\lor g(x))$$$

Lean4

@[continuity, fun_prop]
theorem sup [Max L] [ContinuousSup L] {f g : X → L} (hf : Continuous f) (hg : Continuous g) :
    Continuous fun x => f x ⊔ g x :=
  continuous_sup.comp (hf.prodMk hg :)

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