instBoundedOrderSubtypeSubmoduleMemSublatticeInvtRootSubmodule

English

The collection of submodules represented inside P.invtRootSubmodule forms a bounded order (with top and bottom inherited from Submodule).

Русский

Множество подпространств, входящих в P.invtRootSubmodule, образует ограниченный порядковый структур.

LaTeX

$$$$ \text{BoundedOrder}\; (\{ q \mid q \in P.invtRootSubmodule \}) $$$$

Lean4

instance : BoundedOrder P.invtRootSubmodule
    where
  top := ⟨⊤, invtRootSubmodule.top_mem P⟩
  bot := ⟨⊥, invtRootSubmodule.bot_mem P⟩
  le_top := fun ⟨p, hp⟩ ↦ by simp
  bot_le := fun ⟨p, hp⟩ ↦ by simp

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