tendsto_inf — Mathlib

English

Tendsto f x (y1 ⊓ y2) is equivalent to Tendsto f x y1 and Tendsto f x y2.

Русский

Tendsto f x (y1 ⊓ y2) эквивалентно (Tendsto f x y1) и (Tendsto f x y2).

LaTeX

$$$\\forall f:\\alpha \\to \\beta, \\forall x:\\mathrm{Filter}(\\alpha), \\forall y_1,y_2:\\mathrm{Filter}(\\beta),\\; \\mathrm{Tendsto} f x (y_1 \\sqcap y_2) \\iff \\mathrm{Tendsto} f x y_1 \\land \\mathrm{Tendsto} f x y_2$$$

Lean4

theorem tendsto_inf {f : α → β} {x : Filter α} {y₁ y₂ : Filter β} :
    Tendsto f x (y₁ ⊓ y₂) ↔ Tendsto f x y₁ ∧ Tendsto f x y₂ := by simp only [Tendsto, le_inf_iff]

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