mem_sup_left — Mathlib

English

Let S and T be submodules of a module M over a semiring R. If x belongs to S, then x also belongs to the sum S + T (the join in the submodule lattice).

Русский

Пусть S и T — подмодули модуля M над полугруппой R. Если элемент x принадлежит S, то он принадлежит сумме S + T (наибольшая общая надмножественная подмодуля S и T).

LaTeX

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

Lean4

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

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