le

Mathlib.Analysis.Real.Hyperreal

URI: https://scilib.ai/kg/mathlib#Hyperreal.IsSt.le

English

If x IsSt r and y IsSt s with x ≤ y, then r ≤ s.

Русский

Если x IsSt r и y IsSt s и x ≤ y, то r ≤ s.

LaTeX

$$$\forall {x y} {r s}, \; x.IsSt r \to y.IsSt s \to x \le y \to r \le s$$$

Lean4

theorem le {x y : ℝ*} {r s : ℝ} (hrx : IsSt x r) (hsy : IsSt y s) (hxy : x ≤ y) : r ≤ s :=
  not_lt.1 fun h ↦ hxy.not_gt <| hsy.lt hrx h

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

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

Разделы

Аффилиация

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