prod_mono — Mathlib

English

If s1 ≤ s2 in R and t1 ≤ t2 in S, then s1.prod t1 ≤ s2.prod t2 as subrings of R × S.

Русский

Если s1 ≤ s2 и t1 ≤ t2, то s1.prod t1 ≤ s2.prod t2 как подполья в R × S.

LaTeX

$$$(s_1 \le s_2) \wedge (t_1 \le t_2) \rightarrow s_1.prod t_1 \le s_2.prod t_2$$$

Lean4

@[mono]
theorem prod_mono ⦃s₁ s₂ : NonUnitalSubring R⦄ (hs : s₁ ≤ s₂) ⦃t₁ t₂ : NonUnitalSubring S⦄ (ht : t₁ ≤ t₂) :
    s₁.prod t₁ ≤ s₂.prod t₂ :=
  Set.prod_mono hs ht

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