mul_mem_sup — Mathlib

English

Let S and T be nonunital star subalgebras of A over R. If x ∈ S and y ∈ T, then the product x y lies in the join S ⊔ T.

Русский

Пусть S и T — неполунитарные подалгебры A над R. Если x ∈ S и y ∈ T, то произведение x y принадлежит объединению S ⊔ T.

LaTeX

$$$x \\in S \\land y \\in T \\Rightarrow x y \\in S \\;\\sqcup\\; T$$$

Lean4

theorem mul_mem_sup {S T : NonUnitalStarSubalgebra 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)

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