sub_self

Mathlib.Data.EReal.Operations

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

English

If x ≠ ⊤ and x ≠ ⊥, then x − x = 0.

Русский

Если x ≠ ⊤ и x ≠ ⊥, то x − x = 0.

LaTeX

$$$$x \neq \top \land x \neq \bot \Rightarrow x - x = 0.$$$$

Lean4

@[simp]
theorem sub_self {x : EReal} (h_top : x ≠ ⊤) (h_bot : x ≠ ⊥) : x - x = 0 := by cases x <;> simp_all [← coe_sub]

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

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

Разделы

Аффилиация

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