tendsto_inf_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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