continuous_sup — Mathlib

English

If f,g: X → L are continuous into a lattice L with a ContinuousSup, then the map x ↦ f(x) ⊔ g(x) is continuous.

Русский

Если f,g: X → L непрерывны в решетке L, где операция верхней границы непрерывна, то x ↦ f(x) ⊔ g(x) непрерывна.

LaTeX

$$$\\text{Continuous}(f) \\land \\text{Continuous}(g) \\Rightarrow \\text{Continuous}(x \\mapsto f(x) \\lor g(x))$$$

Lean4

@[continuity]
theorem continuous_sup [Max L] [ContinuousSup L] : Continuous fun p : L × L => p.1 ⊔ p.2 :=
  ContinuousSup.continuous_sup

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