mono_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mono_right {f : α → β} {x : Filter α} {y z : Filter β} (hy : Tendsto f x y) (hz : y ≤ z) : Tendsto f x z :=
  le_trans hy hz

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