leftMulResiduation_le_iff_mul_le — Mathlib

English

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

Русский

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

LaTeX

$$$$ x \le y \;\Longrightarrow\; x \;\text{l-residual } z \;\text{(with respect to } y) \quad \text{iff} \quad x \cdot y \le z $$$$

Lean4

@[to_additive]
theorem leftMulResiduation_le_iff_mul_le : x ≤ y ⇨ₗ z ↔ x * y ≤ z
    where
  mp
    h1 := by
    apply le_trans (mul_le_mul_right' h1 _)
    simp_all only [leftMulResiduation, sSup_mul_distrib, Set.mem_setOf_eq, iSup_le_iff, implies_true]
  mpr h1 := le_sSup h1

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