structure VectorSublattice (X : Type u) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] extends Submodule ℝ X, Sublattice X : Type u

• carrier : Set X
• add_mem' {a b : X} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• smul_mem' (c : ℝ) {x : X} : x ∈ self.carrier → c • x ∈ self.carrier
• supClosed' : SupClosed self.carrier
• infClosed' : InfClosed self.carrier

instance VectorSublattice.instSetLike {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : SetLike (VectorSublattice X) X

Equations

• VectorSublattice.instSetLike = { coe := fun (s : VectorSublattice X) => s.carrier, coe_injective' := ⋯ }

theorem VectorSublattice.ext {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {s t : VectorSublattice X} (h : ∀ (x : X), x ∈ s ↔ x ∈ t) : s = t

theorem VectorSublattice.ext_iff {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {s t : VectorSublattice X} : s = t ↔ ∀ (x : X), x ∈ s ↔ x ∈ t

instance VectorSublattice.instAddCommGroup {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (Y : VectorSublattice X) : AddCommGroup ↥Y

Equations

• Y.instAddCommGroup = Y.toAddSubgroup.toAddCommGroup

instance VectorSublattice.instLattice {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (Y : VectorSublattice X) : Lattice ↥Y

Equations

• Y.instLattice = Y.toSublattice.instLatticeCoe

instance VectorSublattice.instIsOrderedAddMonoid {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (Y : VectorSublattice X) : IsOrderedAddMonoid ↥Y

instance VectorSublattice.instVectorLattice {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (Y : VectorSublattice X) : VectorLattice ↥Y

Equations

• Y.instVectorLattice = { toModule := Y.module, toPosSMulMono := ⋯ }

theorem VectorSublattice.abs_mem {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {Y : VectorSublattice X} {x : X} (h : x ∈ Y) : |x| ∈ Y

def VectorSublattice.ofSubmoduleAbs {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (s : Submodule ℝ X) (h : ∀ x ∈ s, |x| ∈ s) : VectorSublattice X

Equations

• VectorSublattice.ofSubmoduleAbs s h = { carrier := ↑s, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, supClosed' := ⋯, infClosed' := ⋯ }

def VectorSublattice.comap {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {Y : Type u} [AddCommGroup Y] [Lattice Y] [IsOrderedAddMonoid Y] [VectorLattice Y] (f : VecLatHom X Y) (Z : VectorSublattice Y) : VectorSublattice X

Equations

• VectorSublattice.comap f Z = { toSubmodule := Submodule.comap f Z.toSubmodule, supClosed' := ⋯, infClosed' := ⋯ }

structure VectorOrderIdeal (X : Type u) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] extends VectorSublattice X : Type u

• carrier : Set X
• add_mem' {a b : X} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• smul_mem' (c : ℝ) {x : X} : x ∈ self.carrier → c • x ∈ self.carrier
• supClosed' : SupClosed self.carrier
• infClosed' : InfClosed self.carrier
• solid {x y : X} : |x| ≤ |y| → y ∈ self.carrier → x ∈ self.carrier

instance VectorOrderIdeal.instSetLike {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : SetLike (VectorOrderIdeal X) X

Equations

• VectorOrderIdeal.instSetLike = { coe := fun (s : VectorOrderIdeal X) => s.carrier, coe_injective' := ⋯ }

theorem VectorOrderIdeal.ext {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {s t : VectorOrderIdeal X} (h : ∀ (x : X), x ∈ s ↔ x ∈ t) : s = t

theorem VectorOrderIdeal.ext_iff {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {s t : VectorOrderIdeal X} : s = t ↔ ∀ (x : X), x ∈ s ↔ x ∈ t

theorem VectorOrderIdeal.mem_iff_abs_mem {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {I : VectorOrderIdeal X} {x : X} : x ∈ I ↔ |x| ∈ I

theorem VectorOrderIdeal.sub_mem_sup_sub_sup_mem {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {I : VectorOrderIdeal X} {x y y' : X} (h : y - y' ∈ I) : x ⊔ y - x ⊔ y' ∈ I

theorem VectorOrderIdeal.sub_mem_inf_sub_inf_mem {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {I : VectorOrderIdeal X} {x y y' : X} (h : y - y' ∈ I) : x ⊓ y - x ⊓ y' ∈ I

def VectorOrderIdeal.comap {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {Y : Type u} [AddCommGroup Y] [Lattice Y] [IsOrderedAddMonoid Y] [VectorLattice Y] (f : VecLatHom X Y) (Z : VectorOrderIdeal Y) : VectorOrderIdeal X

Equations

• VectorOrderIdeal.comap f Z = { toSubmodule := Submodule.comap f Z.toSubmodule, supClosed' := ⋯, infClosed' := ⋯, solid := ⋯ }

theorem VectorOrderIdeal.mem_comap {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {Y : Type u} [AddCommGroup Y] [Lattice Y] [IsOrderedAddMonoid Y] [VectorLattice Y] (f : VecLatHom X Y) (Z : VectorOrderIdeal Y) (x : X) : x ∈ comap f Z ↔ f x ∈ Z