instBoundedOrderSubtypeSubmoduleMemSublattice

English

The invariant submodules form a bounded order (a bounded lattice) under inclusion, with top and bottom given by V and {0} respectively.

Русский

Инвариантные подподмодули образуют ограниченную по включению решетку; верхний элемент — V, нижний — {0}.

LaTeX

$$$\\rho.invtSubmodule \\text{ is a bounded order with top } = \\top \\text{ and bottom } = \\bot$$$

Lean4

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

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