English
Let M be a partially ordered complete lattice with a multiplication that is monotone on both sides. For every nonempty s with an upper bound and every nonempty t with a lower bound, the supremum of the set of pointwise quotients s/t equals the quotient of the supremum of s by the infimum of t.
Русский
Пусть M — частично упорядоченная полная решетка с умножением, мононтным слева и справа. Для любых непустых s, имеющих верхнюю грань, и непустых t, имеющих нижнюю грань, выполняется: sSup(s/t) = sSup(s) / sInf(t).
LaTeX
$$$\\\\forall M \\\\; [\\\\text{ConditionallyCompleteLattice } M] \\\\; [\\\\text{Group } M] \\\\; [\\\\text{MulLeftMono } M] \\\\; [\\\\text{MulRightMono } M] \\\\; {s, t : Set M}, \\\\; s \\\\neq \\\\emptyset \\\\; \&\\\\; BddAbove s \\\\; \&\\\\; t \\\\neq \\\\emptyset \\\\; \&\\\\; BddBelow t \\\\Rightarrow \\\\ sSup (s / t) = sSup(s) / sInf(t).$$
Lean4
@[to_additive]
theorem csSup_div (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) :
sSup (s / t) = sSup s / sInf t := by
rw [div_eq_mul_inv, csSup_mul hs₀ hs₁ ht₀.inv ht₁.inv, csSup_inv ht₀ ht₁, div_eq_mul_inv]
