sup_mem — Mathlib

English

If p and q are f-invariant submodules of M, then their join p ⊔ q is f-invariant.

Русский

Если p и q — подмодули M, инвариантные относительно f, то их сумма p ⊔ q тоже инвариантна относительно f.

LaTeX

$$$\forall p\,\forall q:\ Submodule\ R\, M,\; p\in f.invtSubmodule \land q\in f.invtSubmodule \Rightarrow p \sqcup q\in f.invtSubmodule$$$

Lean4

theorem sup_mem {p q : Submodule R M} (hp : p ∈ f.invtSubmodule) (hq : q ∈ f.invtSubmodule) : p ⊔ q ∈ f.invtSubmodule :=
  Sublattice.sup_mem hp hq

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