add_mem_sup — Mathlib

English

If S and T are submodules and s ∈ S, t ∈ T, then s + t ∈ S + T, i.e., the sum of two elements from the respective submodules lies in their join.

Русский

Пусть S и T — подмодули, и s ∈ S, t ∈ T. Тогда s + t ∈ S + T, то есть сумма элементов из подмодулей принадлежит их объединению.

LaTeX

$$$\\forall S,T \\; (s \\in S) \\land (t \\in T) \\Rightarrow (s + t) \\in S \\oplus T$$$

Lean4

theorem add_mem_sup {S T : Submodule R M} {s t : M} (hs : s ∈ S) (ht : t ∈ T) : s + t ∈ S ⊔ T :=
  add_mem (mem_sup_left hs) (mem_sup_right ht)

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