mul_mem_sup — Mathlib

English

If x ∈ S and y ∈ T for subsemigroups S, T of M, then the product x y lies in the join S ⊔ T.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mul_mem_sup {S T : Subsemigroup M} {x y : M} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T :=
  mul_mem (mem_sup_left hx) (mem_sup_right hy)

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