bot_mul

Mathlib.Algebra.Order.Quantale

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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