sInf_mul — Mathlib

English

Let s and t be subsets of a suitable ordered group with multiplication, forming a complete lattice; the infimum of the product is the product of the infima: sInf(s * t) = sInf(s) * sInf(t).

Русский

Пусть s и t — подмножества упорядоченной группы с умножением, образующие полную решётку; инфимум произведения равен произведению инфимумов: sInf(s t) = sInf(s) sInf(t).

LaTeX

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

Lean4

@[to_additive]
theorem sInf_mul : sInf (s * t) = sInf s * sInf t :=
  (sInf_image2_eq_sInf_sInf fun _ => (OrderIso.mulRight _).symm.to_galoisConnection) fun _ =>
    (OrderIso.mulLeft _).symm.to_galoisConnection

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