English
Let L and X be topological spaces equipped with a lattice structure on L and a continuous supremum operation. If f,g: X → L are continuous within a set s at a point x, then the pointwise supremum a ↦ f(a) ⊔ g(a) is continuous within s at x.
Русский
Пусть L и X — топологические пространства, на L задана решётка с непрерывной операцией верхней грани. Тогда для любых функций f,g: X → L и множества s ⊆ X, точка x ∈ X, если f и g непрерывны внутри s в x, то их поэлементный максимум (f ⊔ g) также непрерывен внутри s в x.
LaTeX
$$$\\forall L X\\ [TopologicalSpace L]\\ [TopologicalSpace X]\\ [Max L]\\ [ContinuousSup L],\\ \\forall f,g:X \\to L,\\ \\forall s:\\!\\text{Set } X,\\ \\forall x:X,\\ (ContinuousWithinAt\\ f\\ s\\ x \\land ContinuousWithinAt\\ g\\ s\\ x) \\Rightarrow ContinuousWithinAt\\ (\\lambda a \\mapsto f\\,a \\;\\sqcup\\; g\\,a)\\ s\\ x.$$$
Lean4
theorem sup' (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) : ContinuousWithinAt (f ⊔ g) s x :=
hf.sup_nhds' hg
