div_bot

Mathlib.Algebra.Order.Interval.Basic

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

English

There is a division by bottom: s / ⊥ = ⊥ and ⊥ / t = ⊥.

Русский

Деление на нижний элемент: s / ⊥ = ⊥ и ⊥ / t = ⊥.

LaTeX

$$$s / \bot = \bot$ and $\bot / t = \bot$$$

Lean4

@[simp]
theorem div_bot : s / ⊥ = ⊥ :=
  WithBot.map₂_bot_right _ _

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

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

Разделы

Аффилиация

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