sup' — Mathlib

English

If f and g are continuous functions from X to L, then their pointwise supremum is continuous: f ⊔ g is continuous.

Русский

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

LaTeX

$$$\\forall L X\\ [TopologicalSpace L]\\ [TopologicalSpace X]\\ [Min L]?\\ [ContinuousSup L],\\ \\forall f,g:X \\to L,\\ Continuous f\\ \\land\\ Continuous g\\Rightarrow Continuous (\\lambda a \\mapsto f\\ a \\;\\sqcup\\; g\\ a).$$$

Lean4

theorem sup' (hf : Continuous f) (hg : Continuous g) : Continuous (f ⊔ g) :=
  hf.sup hg

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