csInf_mul — Mathlib

English

If s and t are nonempty and bounded below, then the infimum of s t equals the product of the infima of s and t.

Русский

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

LaTeX

$$s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sInf (s * t) = sInf s * sInf t$$

Lean4

@[to_additive]
theorem csInf_mul (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) :
    sInf (s * t) = sInf s * sInf t :=
  csInf_image2_eq_csInf_csInf (fun _ => (OrderIso.mulRight _).symm.to_galoisConnection)
    (fun _ => (OrderIso.mulLeft _).symm.to_galoisConnection) hs₀ hs₁ ht₀ ht₁

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