rightMulResiduation

Mathlib.Algebra.Order.Quantale

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

Lean4

/-- Left- and right- residuation operators on a quantale are similar to the Heyting
operator on complete lattices, but for a non-commutative logic.
I.e. `x ≤ y ⇨ᵣ z ↔ y * x ≤ z` or alternatively `x ⇨ₗ y = sSup { z | x * z ≤ y }`.
-/
@[to_additive existing]
def rightMulResiduation (x y : α) :=
  sSup {z | x * z ≤ y}

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

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

Разделы

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

Аффилиация

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