inf_mul_sup — Mathlib

English

In a lattice-ordered commutative group, the infimum and supremum satisfy (a ∧ b)·(a ∨ b) = a·b.

Русский

В коммутативной группе с упорядочиванием: (a ∧ b)·(a ∨ b) = a·b.

LaTeX

$$$ (a \wedge b) \cdot (a \vee b) = a \cdot b $$$

Lean4

@[to_additive]
theorem inf_mul_sup [MulLeftMono α] (a b : α) : (a ⊓ b) * (a ⊔ b) = a * b :=
  calc
    (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹)) := by
      rw [mul_sup b⁻¹ a⁻¹ (a * b), mul_inv_cancel_right, mul_inv_cancel_comm]
    _ = (a ⊓ b) * (a * b * (a ⊓ b)⁻¹) := by rw [inv_inf, sup_comm]
    _ = a * b := by rw [mul_comm, inv_mul_cancel_right]

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