sup — Mathlib

English

If f,g: X → L are continuous at a point x, then the supremum is continuous at x.

Русский

Если f и g непрерывны в точке x, то их верхняя грань непрерывна в x.

LaTeX

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

Lean4

@[fun_prop]
theorem sup (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun a ↦ f a ⊔ g a) x :=
  hf.sup' hg

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