mem_sup_right — Mathlib

English

Let S and T be submodules of M. If x ∈ T, then x ∈ S + T, i.e., any element of T lies in the sum S + T.

Русский

Пусть S и T — подмодули M. Если x ∈ T, то x ∈ S + T, то есть любой элемент T принадлежит сумме S + T.

LaTeX

$$$\\forall S,T \\; (x \\in T) \\Rightarrow (x \\in S \\oplus T)$$$

Lean4

theorem mem_sup_right {S T : Submodule R M} : ∀ {x : M}, x ∈ T → x ∈ S ⊔ T :=
  by
  have : T ≤ S ⊔ T := le_sup_right
  rw [LE.le] at this
  exact this

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