div_inf — Mathlib

English

In a lattice-ordered group, left-division distributes over the infimum: c / (a ∧ b) = (c / a) ∨ (c / b).

Русский

В упорядоченной по частично упорядоченной группе с операцией умножения слева инфимум распределяет деление слева: c / (a ∧ b) = (c / a) ∨ (c / b).

LaTeX

$$$ c / (a \wedge b) = (c / a) \vee (c / b) $$$

Lean4

@[to_additive]
theorem div_inf (a b c : α) : c / (a ⊓ b) = c / a ⊔ c / b :=
  (OrderIso.divLeft c).map_inf _
    _
      -- In fact 0 ≤ n•a implies 0 ≤ a, see L. Fuchs, "Partially ordered algebraic systems"
      -- Chapter V, 1.E
      -- See also `one_le_pow_iff` for the existing version in linear orders

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