English
Let M be a ConditionallyCompleteLattice carrying a group structure with left and right monotone multiplication. For every nonempty s with a lower bound and every nonempty t with an upper bound, the infimum of s/t equals the quotient of the infimum of s by the supremum of t.
Русский
Пусть M — условно полная решетка с групповой структурой и монотонным умножением слева и справа. Для любых непустых s с нижней гранью и непустых t с верхней гранью выполнено: sInf(s/t) = sInf(s) / sSup(t).
LaTeX
$$$\\\\forall M \\\\; [\\\\text{ConditionallyCompleteLattice } M] \\\\; [\\\\text{Group } M] \\\\; [\\\\text{MulLeftMono } M] \\\\; [\\\\text{MulRightMono } M] \\\\; {s, t : Set M}, \\\\; s \\\\neq \\\\emptyset \\\\; \&\\\\; BddBelow s \\\\; \&\\\\; t \\\\neq \\\\emptyset \\\\; \&\\\\; BddAbove t \\\\Rightarrow \\\\ sInf (s / t) = sInf(s) / sSup(t).$$
Lean4
@[to_additive]
theorem csInf_div (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) :
sInf (s / t) = sInf s / sSup t := by
rw [div_eq_mul_inv, csInf_mul hs₀ hs₁ ht₀.inv ht₁.inv, csInf_inv ht₀ ht₁, div_eq_mul_inv]
