sub_pos

Mathlib.Data.EReal.Operations

URI: https://scilib.ai/kg/mathlib#EReal.sub_pos

English

0 < x − y iff y < x.

Русский

0 < x − y тогда и только тогда y < x.

LaTeX

$$$$0 < x - y \iff y < x.$$$$

Lean4

theorem sub_pos {x y : EReal} : 0 < x - y ↔ y < x := by cases x <;> cases y <;> simp [← EReal.coe_sub]

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

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

Разделы

Аффилиация

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