instIsDirectedSubtypeSubmoduleFGLe

English

The FG-submodules form a directed set under inclusion: given N1 and N2, there exists N with N1 ≤ N and N2 ≤ N, and N is finitely generated.

Русский

Подмодули конечной размерности образуют направленное множество по включению: даны N1,N2, найдётся N, такой что N1 ≤ N, N2 ≤ N и N FG.

LaTeX

$$$\\forall N_1,N_2 \\; (N_1,N_2 \\text{ FG}) \\; \\exists N \\; (N_1 \\le N \\land N_2 \\le N).$$$

Lean4

instance : IsDirected { N : Submodule R M // N.FG } (· ≤ ·) where
  directed N₁ N₂ := ⟨⟨_, N₁.2.sup N₂.2⟩, Subtype.coe_le_coe.mp le_sup_left, Subtype.coe_le_coe.mp le_sup_right⟩

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