prod_mono — Mathlib

English

If L1 ≤ L2 are Sublattices of α and M1 ≤ M2 are Sublattices of β, then the product respects this order: L1.prod M1 ≤ L2.prod M2.

Русский

Пусть L1 ≤ L2 — подпредел(α) и M1 ≤ M2 — подпредел(β). Тогда их произведение удовлетворяет той же частоте отношения: L1.prod M1 ≤ L2.prod M2.

LaTeX

$$$L_1 \\prod M_1 \\le L_2 \\prod M_2$ при $L_1 \\le L_2$ и $M_1 \\le M_2$$$

Lean4

@[gcongr]
theorem prod_mono {L₁ L₂ : Sublattice α} {M₁ M₂ : Sublattice β} (hL : L₁ ≤ L₂) (hM : M₁ ≤ M₂) :
    L₁.prod M₁ ≤ L₂.prod M₂ :=
  Set.prod_mono hL hM

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