sub_bot

Mathlib.Data.EReal.Operations

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

English

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

Русский

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

LaTeX

$$$$x - \bot = \top \\text{ for } x \neq \bot.$$$$

Lean4

@[simp]
theorem sub_bot {x : EReal} (h : x ≠ ⊥) : x - ⊥ = ⊤ := by cases x <;> tauto

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

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

Разделы

Аффилиация

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