mul_mem_sup — Mathlib

English

If x ∈ S and y ∈ T, then the product x y lies in S ⊔ T.

Русский

Если x ∈ S и y ∈ T, то произведение x y принадлежит S ⊔ T.

LaTeX

$$$ \\forall S,T : \\mathrm{NonUnitalSubalgebra}\\, R\\, A,\\; x \\in S, \\; y \\in T \\; \\Rightarrow \\; x y \\in S \\sqcup T $$$

Lean4

theorem mul_mem_sup {S T : NonUnitalSubalgebra R A} {x y : A} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T :=
  mul_mem (mem_sup_left hx) (mem_sup_right hy)

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