mul_bot

Mathlib.Algebra.Order.Quantale

URI: https://scilib.ai/kg/mathlib#Quantale.mul_bot

← MathLib Explorer

English

In a quantale, the bottom element is absorbing on the right: x * ⊥ = ⊥ for all x.

Русский

Ноль справа поглощает умножение: x * ⊥ = ⊥ для всех x.

LaTeX

$$$$ x \cdot \bot = \bot $$$$

Lean4

@[to_additive (attr := simp)]
theorem mul_bot : x * ⊥ = ⊥ := by
  rw [← sSup_empty, mul_sSup_distrib]
  simp only [Set.mem_empty_iff_false, not_false_eq_true, iSup_neg, iSup_bot, sSup_empty]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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