instance VectorOrderIdeal.instBot {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : Bot (VectorOrderIdeal X)

Equations

• VectorOrderIdeal.instBot = { bot := let __src := ⊥; { toSubmodule := __src, supClosed' := ⋯, infClosed' := ⋯, solid := ⋯ } }

theorem VectorOrderIdeal.bot_carrier {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : ⊥.carrier = {0}

theorem VectorOrderIdeal.mem_bot {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {x : X} : x ∈ ⊥ ↔ x = 0

instance VectorOrderIdeal.instTop {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : Top (VectorOrderIdeal X)

Equations

• VectorOrderIdeal.instTop = { top := let __src := ⊤; { toSubmodule := __src, supClosed' := ⋯, infClosed' := ⋯, solid := ⋯ } }

theorem VectorOrderIdeal.top_coe {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : ↑⊤ = Set.univ

instance VectorOrderIdeal.instLE {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : LE (VectorOrderIdeal X)

Equations

• VectorOrderIdeal.instLE = { le := fun (I J : VectorOrderIdeal X) => I.carrier ⊆ J.carrier }

instance VectorOrderIdeal.instBoundedOrder {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : BoundedOrder (VectorOrderIdeal X)

Equations

• VectorOrderIdeal.instBoundedOrder = { toTop := VectorOrderIdeal.instTop, le_top := ⋯, toBot := VectorOrderIdeal.instBot, bot_le := ⋯ }