def PrincipalIdeal {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) : Set X

Equations

• PrincipalIdeal a = {x : X | ∃ (s : ℝ), 0 ≤ s ∧ |x| ≤ s • a}

instance PrincipalIdeal.instAddCommGroup {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) : AddCommGroup ↑(PrincipalIdeal a)

Equations

• PrincipalIdeal.instAddCommGroup a = inferInstance

instance PrincipalIdeal.instLattice {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) : Lattice ↑(PrincipalIdeal a)

Equations

• PrincipalIdeal.instLattice a = inferInstance

instance PrincipalIdeal.instIsOrderedAddMonoid {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) : IsOrderedAddMonoid ↑(PrincipalIdeal a)

instance PrincipalIdeal.instVectorLattice {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) : VectorLattice ↑(PrincipalIdeal a)

Equations

• PrincipalIdeal.instVectorLattice a = inferInstance

theorem PrincipalIdeal.gen_mem {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) (apos : 0 ≤ a) : a ∈ PrincipalIdeal a

theorem PrincipalIdeal.posPart_mem_PI_negPart {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) (h : a⁺ ∈ PrincipalIdeal a⁻) : a⁺ = 0

theorem PrincipalIdeal.bot_iff_zero {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) (apos : 0 ≤ a) : PrincipalIdeal a = ↑⊥ ↔ a = 0