sSup_div — Mathlib

English

In a ConditionallyCompleteLattice with a Group structure, for any s,t with appropriate non-emptiness and bounds, the supremum of s/t equals sSup(s) divided by sInf(t): sSup(s/t) = sSup(s)/sInf(t).

Русский

В условно полной решётке с групповой структурой для любых множества s,t с подходящей непустотой и ограничениями: sSup(s/t) = sSup(s)/sInf(t).

LaTeX

$$$$ \\operatorname{sSup}(s / t) = \\operatorname{sSup}(s) / \\operatorname{sInf}(t). $$$$

Lean4

@[to_additive]
theorem sSup_div : sSup (s / t) = sSup s / sInf t := by simp_rw [div_eq_mul_inv, sSup_mul, sSup_inv]

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