csSup_mul — Mathlib

English

If s and t are nonempty and bounded above, then the supremum of s t equals the product of the sups of s and t.

Русский

Если множества s и t непусты и ограничены сверху, то супремум произведения s t равен произведению супремумов s и t.

LaTeX

$$s.Nonempty → BddAbove s → t.Nonempty → BddAbove t → sSup (s * t) = sSup s * sSup t$$

Lean4

@[to_additive]
theorem csSup_mul (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) :
    sSup (s * t) = sSup s * sSup t :=
  csSup_image2_eq_csSup_csSup (fun _ => (OrderIso.mulRight _).to_galoisConnection)
    (fun _ => (OrderIso.mulLeft _).to_galoisConnection) hs₀ hs₁ ht₀ ht₁

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