theorem UnitalAMSpace.top_iff_unit_mem {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : X) [IsUnitalAMSpace X e] (I : VectorOrderIdeal X) : I = ⊤ ↔ e ∈ I

def UnitalAMSpace.Maximal.above {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) : Set (VectorOrderIdeal X)

Equations

• UnitalAMSpace.Maximal.above I = {J : VectorOrderIdeal X | I.carrier ⊆ J.carrier ∧ J ≠ ⊤}

theorem UnitalAMSpace.Maximal.above_proper {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : X) [IsUnitalAMSpace X e] (I : VectorOrderIdeal X) (J : ↑(above I)) : e ∉ ↑J

theorem UnitalAMSpace.Maximal.above_contains {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) (hI : I ≠ ⊤) : I ∈ above I

instance UnitalAMSpace.Maximal.instPreorderElemVectorOrderIdealAbove {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) : Preorder ↑(above I)

Equations

• UnitalAMSpace.Maximal.instPreorderElemVectorOrderIdealAbove I = { toLE := Subtype.instLE, toLT := Subtype.instLT, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

def UnitalAMSpace.Maximal.nonempty_chain_union {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) (c : Set ↑(above I)) (ne : c.Nonempty) (hc : IsChain (fun (x1 x2 : ↑(above I)) => x1 ≤ x2) c) : VectorOrderIdeal X

Equations

• UnitalAMSpace.Maximal.nonempty_chain_union I c ne hc = { carrier := ⋃ J ∈ c, ↑↑J, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, supClosed' := ⋯, infClosed' := ⋯, solid := ⋯ }

theorem UnitalAMSpace.Maximal.nonempty_chain_union_in_above {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : X) [IsUnitalAMSpace X e] (I : VectorOrderIdeal X) (c : Set ↑(above I)) (ne : c.Nonempty) (hc : IsChain (fun (x1 x2 : ↑(above I)) => x1 ≤ x2) c) : nonempty_chain_union I c ne hc ∈ above I

theorem UnitalAMSpace.Maximal.chain_bddabove {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : X) [IsUnitalAMSpace X e] (I : VectorOrderIdeal X) (hI : I ≠ ⊤) (c : Set ↑(above I)) (hc : IsChain (fun (x1 x2 : ↑(above I)) => x1 ≤ x2) c) : BddAbove c

theorem UnitalAMSpace.Maximal.exists_le_maximal {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) (e : X) [IsUnitalAMSpace X e] (hI : I ≠ ⊤) : ∃ (M : VectorOrderIdeal X), Maximal.IsMaximal M ∧ I ≤ M