class VectorLattice (X : Type u_1) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] extends Module ℝ X, PosSMulMono ℝ X : Type u_1

• smul : ℝ → X → X
• one_smul (b : X) : 1 • b = b
• mul_smul (x y : ℝ) (b : X) : (x * y) • b = x • y • b
• smul_zero (a : ℝ) : a • 0 = 0
• smul_add (a : ℝ) (x y : X) : a • (x + y) = a • x + a • y
• add_smul (r s : ℝ) (x : X) : (r + s) • x = r • x + s • x
• zero_smul (x : X) : 0 • x = 0
• smul_le_smul_of_nonneg_left ⦃a : ℝ⦄ (ha : 0 ≤ a) ⦃b₁ b₂ : X⦄ (hb : b₁ ≤ b₂) : a • b₁ ≤ a • b₂

theorem abs_eq_zero_iff_zero {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (x : X) : |x| = 0 ↔ x = 0

theorem uniqueness_posPart {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (x : X) {u v : X} (hdif : x = u - v) (udisv : u ⊓ v = 0) : u = x⁺

theorem leq_posPart_negPart {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (x y : X) : x ≤ y ↔ x⁺ ≤ y⁺ ∧ y⁻ ≤ x⁻

theorem Riesz_decomposition {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (x y z : X) (xnonneg : 0 ≤ x) (ynonneg : 0 ≤ y) (znonneg : 0 ≤ z) (h : x ≤ y + z) : ∃ (x1 : X) (x2 : X), 0 ≤ x1 ∧ x1 ≤ y ∧ 0 ≤ x2 ∧ x2 ≤ z ∧ x = x1 + x2

theorem nonneg_smul_sup {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x y : X) (a : ℝ) (nonneg : a ≥ 0) : a • (x ⊔ y) = a • x ⊔ a • y

theorem nonneg_smul_inf {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x y : X) (a : ℝ) (nonneg : a ≥ 0) : a • (x ⊓ y) = a • x ⊓ a • y

theorem sup_smul_nonneg {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x : X) (a b : ℝ) (h : 0 ≤ x) : max a b • x = a • x ⊔ b • x

theorem inf_smul_nonneg {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x : X) (a b : ℝ) (h : 0 ≤ x) : min a b • x = a • x ⊓ b • x

theorem abs_smul' {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x : X) (a : ℝ) : |a • x| = |a| • |x|

theorem disjoint_smul {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x y : X) (a : ℝ) (nonneg : 0 ≤ a) (h : x ⊓ y = 0) : a • x ⊓ y = 0

theorem infinitesimal_is_zero {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [Archimedean X] {x y : X} (infinitesimal : ∀ (n : ℕ), n • |x| ≤ y) : x = 0

theorem arch' {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] {x y : X} (h : ∀ (n : ℕ), n • x ≤ y) : x ≤ 0

noncomputable instance instVectorLatticeReal : VectorLattice ℝ

Equations

• instVectorLatticeReal = { toModule := inferInstance, toPosSMulMono := instVectorLatticeReal._proof_1 }