prod_mono — Mathlib

English

If S ≤ T and S₁ ≤ T₁ for nonunital subalgebras, then S.prod S₁ ≤ T.prod T₁.

Русский

Если S ⊆ T и S₁ ⊆ T₁ для неединичных подпалгебр, то произведение удовлетворяет инклюзии.

LaTeX

$$prod_mono : S ≤ T → S₁ ≤ T₁ → prod S S₁ ≤ prod T T₁$$

Lean4

theorem prod_mono {S T : NonUnitalSubalgebra R A} {S₁ T₁ : NonUnitalSubalgebra R B} :
    S ≤ T → S₁ ≤ T₁ → prod S S₁ ≤ prod T T₁ :=
  Set.prod_mono

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