st_le_of_le — Mathlib

English

If not infinite x and not infinite y and x ≤ y, then st(x) ≤ st(y).

Русский

Если x и y не бесконечно велики, и x ≤ y, то st(x) ≤ st(y).

LaTeX

$$$\forall {x y}, \; \neg \mathrm{Infinite}(x) \land \neg \mathrm{Infinite}(y) \land x \le y \Rightarrow \mathrm{st}(x) \le \mathrm{st}(y)$$$

Lean4

theorem st_le_of_le {x y : ℝ*} (hix : ¬Infinite x) (hiy : ¬Infinite y) : x ≤ y → st x ≤ st y :=
  (isSt_st' hix).le (isSt_st' hiy)

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