bot_div

Mathlib.Algebra.Order.Interval.Basic

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

English

There is a division operation on Interval α satisfying s / ⊥ = ⊥.

Русский

Существует операция деления на Interval α так, что s / ⊥ = ⊥.

LaTeX

$$$s / \bot = \bot$$$

Lean4

@[simp]
theorem bot_div : ⊥ / t = ⊥ :=
  WithBot.map₂_bot_left _ _

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

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

Разделы

Аффилиация

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