sInf_div — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem sInf_div : sInf (s / t) = sInf s / sSup t := by simp_rw [div_eq_mul_inv, sInf_mul, sInf_inv]

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