sub_bot

Mathlib.Algebra.Order.Interval.Basic

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

English

Subtracting the bottom element yields bottom: s - ⊥ = ⊥.

Русский

Вычитание нижнего элемента даёт нижний элемент: s - ⊥ = ⊥.

LaTeX

$$$s - \bot = \bot$$$

Lean4

@[simp]
theorem sub_bot : s - ⊥ = ⊥ :=
  WithBot.map₂_bot_right _ _

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

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

Разделы

Аффилиация

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