instance Quotient.instHasQuotient {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : HasQuotient X (VectorOrderIdeal X)

Equations

• Quotient.instHasQuotient = { quotient' := fun (I : VectorOrderIdeal X) => Quotient I.quotientRel }

instance Quotient.instAddCommGroup {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) : AddCommGroup (X ⧸ I)

Equations

• Quotient.instAddCommGroup I = Submodule.Quotient.addCommGroup I.toSubmodule

instance Quotient.instModule {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) : Module ℝ (X ⧸ I)

Equations

• Quotient.instModule I = Submodule.Quotient.module I.toSubmodule

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

Equations

• Quotient.instLE I = { le := fun (a b : X ⧸ I) => ∃ (x : X), 0 ≤ x ∧ I.mkQ x = b - a }

def Quotient.quot_sup {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) : X ⧸ I → X ⧸ I → X ⧸ I

Equations

• Quotient.quot_sup I = Quotient.lift (fun (x : X) => Quotient.lift ((fun (x y : X) => I.mkQ (x ⊔ y)) x) ⋯) ⋯

theorem Quotient.mkQ_map_sup {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) (x y : X) : I.mkQ (x ⊔ y) = quot_sup I (I.mkQ x) (I.mkQ y)

def Quotient.quot_inf {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) : X ⧸ I → X ⧸ I → X ⧸ I

Equations

• Quotient.quot_inf I = Quotient.lift (fun (x : X) => Quotient.lift ((fun (x y : X) => I.mkQ (x ⊓ y)) x) ⋯) ⋯

theorem Quotient.mkQ_map_inf {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) (x y : X) : I.mkQ (x ⊓ y) = quot_inf I (I.mkQ x) (I.mkQ y)

theorem Quotient.lift_inequality {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) {a b : X ⧸ I} (hab : a ≤ b) : ∃ (x : X) (y : X), x ≤ y ∧ I.mkQ x = a ∧ I.mkQ y = b

instance Quotient.instLattice {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) : Lattice (X ⧸ I)

Equations

• One or more equations did not get rendered due to their size.

instance Quotient.instIsOrderedAddMonoid {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) : IsOrderedAddMonoid (X ⧸ I)

instance Quotient.instVectorLattice {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) : VectorLattice (X ⧸ I)

Equations

• Quotient.instVectorLattice I = { toModule := Quotient.instModule I, toPosSMulMono := ⋯ }

def Quotient.mkQ {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) : VecLatHom X (X ⧸ I)

Equations

• Quotient.mkQ I = { toLinearMap := I.mkQ, map_sup' := ⋯, map_inf' := ⋯ }

theorem Quotient.mk_eq_zero {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (I : VectorOrderIdeal X) (x : X) : (mkQ I) x = 0 ↔ x ∈ I