rightMulResiduation_le_iff_mul_le

English

In a quantale, the right residuation operator ⇨ᵣ satisfies: x ≤ y ⇨ᵣ z iff y * x ≤ z, expressing an adjunction between right multiplication and the order.

Русский

В кватале правый резидуальный оператор ⇨ᵣ удовлетворяет: x ≤ y ⇨ᵣ z тогда и только если y * x ≤ z.

LaTeX

$$$$ x \le y \;\Longrightarrow\; x \text{ right-residual } z \;\text{with respect to } y \quad \Longleftrightarrow \quad y \cdot x \le z $$$$

Lean4

@[to_additive]
theorem rightMulResiduation_le_iff_mul_le : x ≤ y ⇨ᵣ z ↔ y * x ≤ z
    where
  mp
    h1 := by
    apply le_trans (mul_le_mul_left' h1 _)
    simp_all only [rightMulResiduation, mul_sSup_distrib, Set.mem_setOf_eq, iSup_le_iff, implies_true]
  mpr h1 := le_sSup h1

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