sub_neg

Mathlib.Data.EReal.Operations

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

← MathLib Explorer

English

x − y < 0 iff x < y.

Русский

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

LaTeX

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

Lean4

theorem sub_neg {x y : EReal} (h_top : x ≠ ⊤ ∨ y ≠ ⊤) (h_bot : x ≠ ⊥ ∨ y ≠ ⊥) : x - y < 0 ↔ x < y := by
  cases x <;> cases y <;> simp_all [← EReal.coe_sub]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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