sup_sup — Mathlib

English

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

Русский

Если Tendsto f x1 y1 и Tendsto f x2 y2, то Tendsto f (x1 ⊔ x2) (y1 ⊔ y2).

LaTeX

$$$ \\operatorname{Tendsto} f x_1 y_1 \\land \\operatorname{Tendsto} f x_2 y_2 \\Rightarrow \\operatorname{Tendsto} f (x_1 \\lor x_2) (y_1 \\lor y_2) $$$

Lean4

theorem sup_sup {f : α → β} {x₁ x₂ : Filter α} {y₁ y₂ : Filter β} (h₁ : Tendsto f x₁ y₁) (h₂ : Tendsto f x₂ y₂) :
    Tendsto f (x₁ ⊔ x₂) (y₁ ⊔ y₂) :=
  tendsto_sup.mpr ⟨h₁.mono_right le_sup_left, h₂.mono_right le_sup_right⟩

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