English
Let f,g: X → L be maps between topological spaces with a lattice structure on L. If f and g are continuous within s at x, then the function a ↦ f(a) ⊔ g(a) is continuous within s at x.
Русский
Пусть f,g: X → L, где L имеет топологическое пространство и решётку с непрерывной операцией верхней грани. Если f и g непрерывны внутри s в точке x, то их точечная сумма f(a) ⊔ g(a) непрерывна внутри 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 (fun a ↦ f a ⊔ g a) s x :=
hf.sup' hg
