sup — Mathlib

English

If f,g : X → L are ContinuousOn f s and ContinuousOn g s, then the supremum function f ⊔ g is ContinuousOn s.

Русский

Если f,g: X → L непрерывны на s, то их точечный максимум f ⊔ g непрерывен на s.

LaTeX

$$$\\forall L X\\ [TopologicalSpace L]\\ [TopologicalSpace X]\\ [Max L]\\ [ContinuousSup L],\\ \\forall f,g:X \\to L,\\ \\forall s:\\!\\text{Set } X,\\ ContinuousOn\\ f\\ s\\ \\land\\ ContinuousOn\\ g\\ s\\Rightarrow ContinuousOn\\ (\\lambda a \\mapsto f\\ a \\;\\sqcup\\; g\\ a)\\ s.$$$

Lean4

@[fun_prop]
theorem sup (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun a ↦ f a ⊔ g a) s :=
  hf.sup' hg

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