lt_sup_iff_notMem — Mathlib

English

For a set of submodules S, an element m ∈ sSup(S) iff m ∈ N for every submodule N that is an upper bound of all members of S.

Русский

Для множества подмодулей S элемент m принадлежит sSup(S) тогда и только тогда, когда m принадлежит любому подмодулю N, являющемуся верхней границей всех членов S.

LaTeX

$$$m \in \mathrm{sSup}(S) \iff \forall N, (\forall p \in S, p \le N) \to m \in N$$$

Lean4

theorem lt_sup_iff_notMem {I : Submodule R M} {a : M} : (I < I ⊔ R ∙ a) ↔ a ∉ I := by simp

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