sup — Mathlib

English

If Tendsto f x1 y and Tendsto f x2 y, then Tendsto f (x1 ⊔ x2) y.

Русский

Если Tendsto f x1 y и Tendsto f x2 y, тогда Tendsto f (x1 ⊔ x2) y.

LaTeX

$$$ \\operatorname{Tendsto} f x_1 y \\wedge \\operatorname{Tendsto} f x_2 y \\Rightarrow \\operatorname{Tendsto} f (x_1 \\lor x_2) y $$$

Lean4

theorem sup {f : α → β} {x₁ x₂ : Filter α} {y : Filter β} : Tendsto f x₁ y → Tendsto f x₂ y → Tendsto f (x₁ ⊔ x₂) y :=
  fun h₁ h₂ => tendsto_sup.mpr ⟨h₁, h₂⟩

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