sup' — Mathlib

English

If f,g: X → L are continuous at a point x, then the map a ↦ f(a) ⊔ g(a) is continuous at x.

Русский

Если f и g непрерывны в точке x, то отображение a ↦ f(a) ⊔ g(a) непрерывно в x.

LaTeX

$$$\\text{hf} : \\text{ContinuousAt}(f,x) \\land \\text{hg} : \\text{ContinuousAt}(g,x) \\Rightarrow \\text{ContinuousAt}(\\lambda a, f(a) \\sqcup g(a), x)$$$

Lean4

theorem sup' (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (f ⊔ g) x :=
  hf.sup_nhds' hg

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