sub_self_le_zero

Mathlib.Data.EReal.Operations

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

English

For all x ∈ EReal, x − x ≤ 0.

Русский

Для всех x ∈ EReal выполнено x − x ≤ 0.

LaTeX

$$$$x - x \le 0.$$$$

Lean4

theorem sub_self_le_zero {x : EReal} : x - x ≤ 0 := by cases x <;> simp

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

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

Разделы

Аффилиация

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