mem_sup — Mathlib

English

An element x lies in the closed-submodule supremum s ⊔ t if and only if x lies in the closure of the sum of s and t as submodules.

Русский

Элемент x принадлежит наибольшему из двух подмодулей, если и только если x принадлежит замыканию суммы подмодулей s и t.

LaTeX

$$$x \in s \sqcup t \iff x \in closure (s.toSubmodule \sqcup t.toSubmodule).carrier$$$

Lean4

@[simp]
theorem mem_sup : x ∈ s ⊔ t ↔ x ∈ closure (s.toSubmodule ⊔ t.toSubmodule).carrier :=
  Iff.rfl

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