mono_left — Mathlib

English

If f: α → β tends from x to z and y ≤ x, then f tends from y to z.

Русский

Если f: α → β стремится от x к z и y вложено в x, то f стремится от y к z.

LaTeX

$$$\\forall f:\\alpha \\to \\beta,\\; \\forall x,y:\\mathrm{Filter}(\\alpha),\\; \\forall z:\\mathrm{Filter}(\\beta),\\; (\\mathrm{Tendsto} f\\ x\\ z) \\land (y \\le x) \\Rightarrow \\mathrm{Tendsto} f\\ y\\ z$$$

Lean4

theorem mono_left {f : α → β} {x y : Filter α} {z : Filter β} (hx : Tendsto f x z) (h : y ≤ x) : Tendsto f y z :=
  (map_mono h).trans hx

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