sub_mem_sup — Mathlib

English

If s ∈ S and t ∈ T, then s − t ∈ S + T; the submodule sum contains both S and T, so it contains differences as well through s − t = s + (−t).

Русский

Если s ∈ S и t ∈ T, то s − t ∈ S + T; сумма подмодулов содержит и вычитания через представление −t.

LaTeX

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

Lean4

theorem sub_mem_sup {R' M' : Type*} [Ring R'] [AddCommGroup M'] [Module R' M'] {S T : Submodule R' M'} {s t : M'}
    (hs : s ∈ S) (ht : t ∈ T) : s - t ∈ S ⊔ T := by
  rw [sub_eq_add_neg]
  exact add_mem_sup hs (neg_mem ht)

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