tendsto_sup — Mathlib

English

Let f: α → β and filters x1, x2 on α and y on β. Then Tendsto f x1 y and Tendsto f x2 y imply Tendsto f (x1 ⊔ x2) y.

Русский

Пусть f: α → β и фильтры x1, x2 на α, y на β. Тогда если Tendsto f x1 y и Tendsto f x2 y, то Tendsto f (x1 ⊔ x2) y.

LaTeX

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

Lean4

@[simp]
theorem tendsto_sup {f : α → β} {x₁ x₂ : Filter α} {y : Filter β} :
    Tendsto f (x₁ ⊔ x₂) y ↔ Tendsto f x₁ y ∧ Tendsto f x₂ y := by simp only [Tendsto, map_sup, sup_le_iff]

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