div_sup — Mathlib

English

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

Русский

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

LaTeX

$$$ c / (a \lor b) = (c / a) \land (c / b) $$$

Lean4

@[to_additive]
theorem div_sup (a b c : α) : c / (a ⊔ b) = c / a ⊓ c / b :=
  (OrderIso.divLeft c).map_sup _ _

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