mem_sSup_of_mem — Mathlib

English

If S is a set of submodules and s ∈ S, then every x ∈ s is also in sSup S, the supremum of S.

Русский

Пусть S — множество подмодулей, и s ∈ S. Тогда каждый x ∈ s принадлежит sSup S, наибольшему верхнему пределу множества S.

LaTeX

$$$\\forall S \\; (s \\in S) \\Rightarrow (x \\in s \\Rightarrow x \\in \\bigvee S)$$$

Lean4

theorem mem_sSup_of_mem {S : Set (Submodule R M)} {s : Submodule R M} (hs : s ∈ S) : ∀ {x : M}, x ∈ s → x ∈ sSup S :=
  by
  have := le_sSup hs
  rw [LE.le] at this
  exact this

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