tendsto_inf_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem tendsto_inf_right {f : α → β} {x₁ x₂ : Filter α} {y : Filter β} (h : Tendsto f x₂ y) : Tendsto f (x₁ ⊓ x₂) y :=
  le_trans (map_mono inf_le_right) h

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