lt_of_st_lt

Mathlib.Analysis.Real.Hyperreal

URI: https://scilib.ai/kg/mathlib#Hyperreal.lt_of_st_lt

English

If not infinite x and not infinite y, and st x < st y, then x < y.

Русский

Если x и y не бесконечно велики, и st(x) < st(y), тогда x < y.

LaTeX

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

Lean4

theorem lt_of_st_lt {x y : ℝ*} (hix : ¬Infinite x) (hiy : ¬Infinite y) : st x < st y → x < y :=
  (isSt_st' hix).lt (isSt_st' hiy)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru