inf — Mathlib

English

Let f: α → β and x1, x2: Filter α; y: Filter β. If f tends to y along x1 and along x2, then f tends to y along x1 ∧ x2.

Русский

Пусть f: α → β и фильтры x1, x2 на α, y на β. Если f сходится к y по x1 и по x2, тогда сходимость по x1 ∧ x2.

LaTeX

$$$ \\operatorname{Tendsto} f x_1 y \\rightarrow \\operatorname{Tendsto} f x_2 y \\rightarrow \\operatorname{Tendsto} f (x_1 \\land x_2) (y_1 \\land y_2) $$$

Lean4

theorem inf {f : α → β} {x₁ x₂ : Filter α} {y₁ y₂ : Filter β} (h₁ : Tendsto f x₁ y₁) (h₂ : Tendsto f x₂ y₂) :
    Tendsto f (x₁ ⊓ x₂) (y₁ ⊓ y₂) :=
  tendsto_inf.2 ⟨tendsto_inf_left h₁, tendsto_inf_right h₂⟩

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