English
Let f,g: X → L be functions with L a topological lattice. If f and g are ContinuousOn f s and ContinuousOn g s, then f ⊔ g is ContinuousOn s.
Русский
Пусть f,g: X → L, L — топологическая решётка. Тогда если f и g непрерывны на множесте 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
theorem sup' (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (f ⊔ g) s := fun x hx ↦
(hf x hx).sup' (hg x hx)
