Order ideals of vector lattices

An order ideal (or simply ideal) of a vector lattice is a sublattice that is solid: if x ∈ J and |y| ≤ |x| then y ∈ J. Equivalently, an ideal is precisely a solid subspace. This file defines the bundled OrderIdeal structure extending VectorSublattice and establishes the basic characterisations and properties.

structure OrderIdeal (X : Type u_2) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] extends VectorSublattice X : Type u_2

An OrderIdeal of a vector lattice X is a vector sublattice that is solid: whenever x ∈ J and 0 ≤ y ≤ x, we have y ∈ J.

• 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
• sup_mem' {x y : X} : x ∈ self.carrier → y ∈ self.carrier → x ⊔ y ∈ self.carrier
• solid' {x y : X} : x ∈ self.carrier → 0 ≤ y → y ≤ x → y ∈ self.carrier

@[instance_reducible]

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

Equations

• OrderIdeal.instSetLike = { coe := fun (J : OrderIdeal X) => J.carrier, coe_injective := ⋯ }

@[instance_reducible]

instance OrderIdeal.instPartialOrder {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : PartialOrder (OrderIdeal X)

Order ideals of X, ordered by inclusion, form a partial order.

Equations

• OrderIdeal.instPartialOrder = PartialOrder.ofSetLike (OrderIdeal X)

theorem OrderIdeal.solid {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (J : OrderIdeal X) {x y : X} (hx : x ∈ J) (hy0 : 0 ≤ y) (hyx : y ≤ x) : y ∈ J

An order ideal is solid: x ∈ J and 0 ≤ y ≤ x imply y ∈ J.

theorem OrderIdeal.sup_mem {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (J : OrderIdeal X) {x y : X} (hx : x ∈ J) (hy : y ∈ J) : x ⊔ y ∈ J

An order ideal is closed under ⊔.

theorem OrderIdeal.inf_mem {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (J : OrderIdeal X) {x y : X} (hx : x ∈ J) (hy : y ∈ J) : x ⊓ y ∈ J

An order ideal is closed under ⊓.

theorem OrderIdeal.abs_mem {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (J : OrderIdeal X) {x : X} (hx : x ∈ J) : |x| ∈ J

An order ideal is closed under absolute value.

theorem OrderIdeal.mem_of_abs_mem {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (J : OrderIdeal X) {x : X} (h : |x| ∈ J) : x ∈ J

If |x| ∈ J then x ∈ J.

theorem OrderIdeal.mem_of_abs_le_abs {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (J : OrderIdeal X) {x y : X} (hx : x ∈ J) (h : |y| ≤ |x|) : y ∈ J

Solidity in terms of absolute value: x ∈ J and |y| ≤ |x| imply y ∈ J.

Construction from solidity

def OrderIdeal.ofSolid {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (M : Submodule ℝ X) (h : ∀ (x y : X), x ∈ M → |y| ≤ |x| → y ∈ M) : OrderIdeal X

Build an OrderIdeal from a submodule that is solid in the absolute-value sense: x ∈ M and |y| ≤ |x| imply y ∈ M. Every solid subspace is automatically a sublattice and an ideal.

Equations

• OrderIdeal.ofSolid M h = { toSubmodule := M, sup_mem' := ⋯, solid' := ⋯ }

theorem OrderIdeal.solid_iff {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (M : Submodule ℝ X) : (∀ (x y : X), x ∈ M → |y| ≤ |x| → y ∈ M) ↔ (∀ (x y : X), x ∈ M → 0 ≤ y → y ≤ x → y ∈ M) ∧ ∀ (x y : X), x ∈ M → y ∈ M → x ⊔ y ∈ M

A submodule is the carrier of an order ideal iff it is solid.

theorem OrderIdeal.toSubmodule_injective {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : Function.Injective fun (J : OrderIdeal X) => J.toSubmodule

The coercion to Submodule ℝ X is injective.

Ideal generated by a set

def OrderIdeal.inf {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (J₁ J₂ : OrderIdeal X) : OrderIdeal X

The intersection of two order ideals is an order ideal.

Equations

• J₁.inf J₂ = { toSubmodule := J₁.toSubmodule ⊓ J₂.toSubmodule, sup_mem' := ⋯, solid' := ⋯ }

@[instance_reducible]

instance OrderIdeal.instInfSet {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : InfSet (OrderIdeal X)

Order ideals of X admit arbitrary intersections: they form a complete semilattice for the ⊓ operation.

Equations

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

@[simp]

theorem OrderIdeal.mem_sInf {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {S : Set (OrderIdeal X)} {x : X} : x ∈ sInf S ↔ ∀ J ∈ S, x ∈ J

Membership in an arbitrary intersection of order ideals.

def OrderIdeal.generated {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (s : Set X) : OrderIdeal X

The ideal generated by a set s ⊆ X is the smallest order ideal of X containing s, defined as the intersection of all order ideals containing s.

Equations

• OrderIdeal.generated s = sInf {J : OrderIdeal X | s ⊆ ↑J}

theorem OrderIdeal.subset_generated {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (s : Set X) : s ⊆ ↑(generated s)

The set s is contained in the ideal it generates.

theorem OrderIdeal.generated_le {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {s : Set X} {J : OrderIdeal X} (h : s ⊆ ↑J) : generated s ≤ J

The ideal generated by s is contained in any ideal containing s.

theorem OrderIdeal.mem_generated_iff {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {s : Set X} {x : X} : x ∈ generated s ↔ ∃ (t : Finset X) (c : X → ℝ), (∀ y ∈ t, y ∈ s) ∧ (∀ y ∈ t, 0 ≤ c y) ∧ |x| ≤ ∑ y ∈ t, c y • |y|

Explicit description of the generated ideal. An element x lies in the ideal generated by s if and only if |x| is bounded above by a non-negative linear combination of absolute values of elements of s.

Principal ideal

def OrderIdeal.principal {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) : OrderIdeal X

The principal ideal generated by a is the set of elements x with |x| ≤ c • |a| for some c ≥ 0.

Equations

• OrderIdeal.principal a = { carrier := {x : X | ∃ (c : ℝ), 0 ≤ c ∧ |x| ≤ c • |a|}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, sup_mem' := ⋯, solid' := ⋯ }

theorem OrderIdeal.mem_principal {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {a x : X} : x ∈ principal a ↔ ∃ (c : ℝ), 0 ≤ c ∧ |x| ≤ c • |a|

Characterisation of membership in the principal ideal.

theorem OrderIdeal.self_mem_principal {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) : a ∈ principal a

The generator belongs to its own principal ideal.

theorem OrderIdeal.principal_eq_generated_abs {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) : principal a = generated {|a|}

The principal ideal generated by a coincides with the ideal generated by the singleton {|a|}.

Gauge norm on the principal ideal

noncomputable def OrderIdeal.gaugeNorm {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a x : X) : ℝ

The gauge norm (or order-unit norm) of x with respect to a is inf {c ≥ 0 | |x| ≤ c • |a|}. For x in the principal ideal of a, this is finite and defines a lattice seminorm; it is a norm precisely when the ambient space is Archimedean.

Equations

• OrderIdeal.gaugeNorm a x = sInf {c : ℝ | 0 ≤ c ∧ |x| ≤ c • |a|}

theorem OrderIdeal.gaugeNorm_nonneg {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a x : X) : 0 ≤ gaugeNorm a x

The gauge norm is non-negative.

theorem OrderIdeal.gaugeNorm_zero {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) : gaugeNorm a 0 = 0

The gauge norm of zero is zero.

theorem OrderIdeal.gaugeNorm_neg {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a x : X) : gaugeNorm a (-x) = gaugeNorm a x

The gauge norm is symmetric.

theorem OrderIdeal.gaugeNorm_add_le {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) {x y : X} (hx : x ∈ principal a) (hy : y ∈ principal a) : gaugeNorm a (x + y) ≤ gaugeNorm a x + gaugeNorm a y

theorem OrderIdeal.gaugeNorm_smul {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) (r : ℝ) (x : X) : gaugeNorm a (r • x) = |r| * gaugeNorm a x

theorem OrderIdeal.abs_le_gaugeNorm_smul_abs {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) [IsVLArchimedean X] {x : X} (hx : x ∈ principal a) : |x| ≤ gaugeNorm a x • |a|

The gauge norm controls the absolute value: |x| ≤ ‖x‖_a • |a| for x in the principal ideal.

theorem OrderIdeal.gaugeNorm_le_of_abs_le {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) {x : X} {c : ℝ} (hc : 0 ≤ c) (h : |x| ≤ c • |a|) : gaugeNorm a x ≤ c

Any admissible constant bounds the gauge norm from above.

theorem OrderIdeal.gaugeNorm_mono_abs {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) {x y : X} (hy : y ∈ principal a) (h : |x| ≤ |y|) : gaugeNorm a x ≤ gaugeNorm a y

The gauge norm is monotone with respect to |·|: the solid-norm property.

theorem OrderIdeal.gaugeNorm_eq_zero_iff {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) [IsVLArchimedean X] {x : X} (hx : x ∈ principal a) : gaugeNorm a x = 0 ↔ x = 0

In an Archimedean vector lattice the gauge norm is definite: gaugeNorm a x = 0 ↔ x = 0 for x in the principal ideal of a.

theorem OrderIdeal.gaugeNorm_le_one_iff {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) [IsVLArchimedean X] {x : X} (hx : x ∈ principal a) : gaugeNorm a x ≤ 1 ↔ |x| ≤ |a|

The closed unit ball of the gauge norm is the order interval [-|a|, |a|].

theorem OrderIdeal.gaugeNorm_anti {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {e u : X} (he : 0 ≤ e) (heu : e ≤ u) {x : X} (hx : x ∈ principal e) : gaugeNorm u x ≤ gaugeNorm e x

If 0 ≤ e ≤ u then ‖·‖_u ≤ ‖·‖_e on I_e.

Normed vector lattice structure on the principal ideal

@[reducible, inline]

abbrev OrderIdeal.principalSubmodule {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) : Submodule ℝ X

The underlying submodule of the principal ideal.

Equations

• OrderIdeal.principalSubmodule a = (OrderIdeal.principal a).toSubmodule

@[instance_reducible]

noncomputable instance OrderIdeal.instNormPrincipal {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) : Norm ↥(principalSubmodule a)

The gauge norm as a Norm instance on the principal ideal.

Equations

• OrderIdeal.instNormPrincipal a = { norm := fun (x : ↥(OrderIdeal.principalSubmodule a)) => OrderIdeal.gaugeNorm a ↑x }

@[instance_reducible]

noncomputable instance OrderIdeal.instLatticePrincipal {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) : Lattice ↥(principalSubmodule a)

The principal ideal inherits a lattice structure from X.

Equations

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

instance OrderIdeal.instIsOrderedAddMonoidPrincipal {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) : IsOrderedAddMonoid ↥(principalSubmodule a)

The principal ideal is an ordered additive monoid.

@[reducible]

noncomputable def OrderIdeal.principalNormedAddCommGroup {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [IsVLArchimedean X] (a : X) : NormedAddCommGroup ↥(principalSubmodule a)

In an Archimedean vector lattice, the principal ideal I_a with the gauge norm is a normed additive commutative group.

Equations

• OrderIdeal.principalNormedAddCommGroup a = NormedAddCommGroup.ofCore ⋯

@[reducible]

noncomputable def OrderIdeal.principalVectorLattice {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : X) : VectorLattice ↥(principalSubmodule a)

In an Archimedean vector lattice, the principal ideal I_a with the gauge norm admits a VectorLattice structure.

Equations

• OrderIdeal.principalVectorLattice a = { toModule := (OrderIdeal.principalSubmodule a).module, toPosSMulMono := ⋯ }

@[reducible]

noncomputable def OrderIdeal.principalNormedVectorLattice {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [IsVLArchimedean X] (a : X) : NormedVectorLattice ↥(principalSubmodule a)

In an Archimedean vector lattice, the principal ideal I_a equipped with the gauge norm is a normed vector lattice.

Equations

• OrderIdeal.principalNormedVectorLattice a = { toVectorLattice := OrderIdeal.principalVectorLattice a, toHasSolidNorm := ⋯, toNormSMulClass := ⋯ }

Sum of ideals

def OrderIdeal.sum {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (J₁ J₂ : OrderIdeal X) : OrderIdeal X

The sum of two order ideals (as submodules) is again an order ideal.

Equations

• J₁.sum J₂ = OrderIdeal.ofSolid (J₁.toSubmodule + J₂.toSubmodule) ⋯

@[simp]

theorem OrderIdeal.sum_toSubmodule {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (J₁ J₂ : OrderIdeal X) : (J₁.sum J₂).toSubmodule = J₁.toSubmodule + J₂.toSubmodule

The underlying submodule of sum J₁ J₂ is J₁.toSubmodule + J₂.toSubmodule.

theorem OrderIdeal.exists_sum_decomp_nonneg {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (J₁ J₂ : OrderIdeal X) {y : X} (hy : y ∈ J₁.toSubmodule + J₂.toSubmodule) (hy0 : 0 ≤ y) : ∃ (y₁ : X) (y₂ : X), y₁ ∈ J₁ ∧ y₂ ∈ J₂ ∧ y₁ + y₂ = y ∧ 0 ≤ y₁ ∧ 0 ≤ y₂

Positive decomposition in the sum of two ideals: every non-negative element of J₁ + J₂ admits a splitting y = y₁ + y₂ with 0 ≤ y₁ ∈ J₁ and 0 ≤ y₂ ∈ J₂.

theorem OrderIdeal.exists_sum_decomp {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (J₁ J₂ : OrderIdeal X) {z : X} (hz : z ∈ J₁.toSubmodule + J₂.toSubmodule) : ∃ (a : X) (b : X), a ∈ J₁ ∧ b ∈ J₂ ∧ a + b = z ∧ |a| ≤ |z| ∧ |b| ≤ |z|

Bounded decomposition in the sum of two ideals: every element of J₁ + J₂ admits a splitting z = a + b with a ∈ J₁, b ∈ J₂ and the lattice estimates |a| ≤ |z|, |b| ≤ |z|.

Complete lattice structure

@[instance_reducible]

instance OrderIdeal.instTop {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : Top (OrderIdeal X)

The whole space X is an order ideal.

Equations

• OrderIdeal.instTop = { top := let __Submodule := ⊤; { toSubmodule := __Submodule, sup_mem' := ⋯, solid' := ⋯ } }

@[simp]

theorem OrderIdeal.mem_top {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {x : X} : x ∈ ⊤

@[instance_reducible]

instance OrderIdeal.instBot {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : Bot (OrderIdeal X)

The trivial ideal {0} is an order ideal.

Equations

• OrderIdeal.instBot = { bot := let __Submodule := ⊥; { toSubmodule := __Submodule, sup_mem' := ⋯, solid' := ⋯ } }

@[simp]

theorem OrderIdeal.mem_bot {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {x : X} : x ∈ ⊥ ↔ x = 0

@[instance_reducible]

instance OrderIdeal.instCompleteLattice {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : CompleteLattice (OrderIdeal X)

Order ideals of X, ordered by inclusion, form a complete lattice. Binary joins are given by the (Minkowski) sum sum, binary meets and arbitrary infima are given by intersection, the bottom element is the trivial ideal {0}, and the top element is the whole space.

Equations

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

@[simp]

theorem OrderIdeal.sup_toSubmodule {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (J₁ J₂ : OrderIdeal X) : (J₁ ⊔ J₂).toSubmodule = J₁.toSubmodule + J₂.toSubmodule

@[simp]

theorem OrderIdeal.inf_toSubmodule {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (J₁ J₂ : OrderIdeal X) : (J₁ ⊓ J₂).toSubmodule = J₁.toSubmodule ⊓ J₂.toSubmodule

Strong order units and the principal ideal

theorem OrderIdeal.strongOrderUnit_iff_principal_eq_top {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {e : X} : StrongOrderUnit e ↔ 0 ≤ e ∧ principal e = ⊤

An element is a strong order unit precisely when it is non-negative and the principal ideal it generates is the whole space.

Existence of proper non-trivial ideals

theorem OrderIdeal.exists_proper_nontrivial {X : Type u_2} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [IsVLArchimedean X] (h : 1 < Module.rank ℝ X) : ∃ (J : OrderIdeal X), J ≠ ⊥ ∧ J ≠ ⊤

If the real dimension of X is strictly greater than one, then X admits an order ideal that is neither trivial nor the whole space.

Closure of an ideal in a normed vector lattice

theorem OrderIdeal.topologicalClosure_solid {X : Type u_3} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] (J : OrderIdeal X) (x y : X) : x ∈ J.topologicalClosure → |y| ≤ |x| → y ∈ J.topologicalClosure

The topological closure of the underlying submodule of an order ideal is itself solid: if x lies in the closure and |y| ≤ |x|, then y lies in the closure.

def OrderIdeal.topologicalClosure {X : Type u_3} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] (J : OrderIdeal X) : OrderIdeal X

The norm closure of an order ideal J in a normed vector lattice is again an order ideal, whose underlying submodule is the topological closure of J.toSubmodule.

Equations

• J.topologicalClosure = OrderIdeal.ofSolid J.topologicalClosure ⋯

@[simp]

theorem OrderIdeal.topologicalClosure_toSubmodule {X : Type u_3} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] (J : OrderIdeal X) : J.topologicalClosure.toSubmodule = J.topologicalClosure

structure ClosedOrderIdeal (X : Type u_2) [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] extends OrderIdeal X : Type u_2

A closed order ideal of a Banach lattice is an order ideal whose underlying set is closed in the norm topology.

• 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
• sup_mem' {x y : X} : x ∈ self.carrier → y ∈ self.carrier → x ⊔ y ∈ self.carrier
• solid' {x y : X} : x ∈ self.carrier → 0 ≤ y → y ≤ x → y ∈ self.carrier
• isClosed' : IsClosed ↑self.toOrderIdeal

@[instance_reducible]

instance ClosedOrderIdeal.instSetLike {X : Type u_2} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] : SetLike (ClosedOrderIdeal X) X

Equations

• ClosedOrderIdeal.instSetLike = { coe := fun (J : ClosedOrderIdeal X) => ↑J.toOrderIdeal, coe_injective := ⋯ }

theorem ClosedOrderIdeal.isClosed {X : Type u_2} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] (J : ClosedOrderIdeal X) : IsClosed ↑J

A closed order ideal is closed as a subset of X.

@[instance_reducible]

instance ClosedOrderIdeal.instPartialOrder {X : Type u_2} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] : PartialOrder (ClosedOrderIdeal X)

Closed order ideals form a partial order under inclusion.

Equations

• ClosedOrderIdeal.instPartialOrder = PartialOrder.ofSetLike (ClosedOrderIdeal X)

def ClosedOrderIdeal.inf {X : Type u_2} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] (J₁ J₂ : ClosedOrderIdeal X) : ClosedOrderIdeal X

The intersection of two closed order ideals is a closed order ideal.

Equations

• J₁.inf J₂ = { toOrderIdeal := J₁.toOrderIdeal ⊓ J₂.toOrderIdeal, isClosed' := ⋯ }

theorem ClosedOrderIdeal.isClosed_sum {X : Type u_2} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] {J₁ J₂ : OrderIdeal X} (h₁ : IsClosed ↑J₁) (h₂ : IsClosed ↑J₂) : IsClosed ↑(J₁.sum J₂)

The sum of two closed order ideals in a Banach lattice is again closed.

def ClosedOrderIdeal.sup {X : Type u_2} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] (J₁ J₂ : ClosedOrderIdeal X) : ClosedOrderIdeal X

The sum of two closed order ideals of a Banach lattice is again a closed order ideal.

Equations

• J₁.sup J₂ = { toOrderIdeal := J₁.sum J₂.toOrderIdeal, isClosed' := ⋯ }

def ClosedOrderIdeal.sInf {X : Type u_2} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] (S : Set (ClosedOrderIdeal X)) : ClosedOrderIdeal X

The arbitrary intersection of a family of closed order ideals is a closed order ideal.

Equations

• ClosedOrderIdeal.sInf S = { toOrderIdeal := sInf ((fun (J : ClosedOrderIdeal X) => J.toOrderIdeal) '' S), isClosed' := ⋯ }

@[instance_reducible]

instance ClosedOrderIdeal.instLattice {X : Type u_2} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] : Lattice (ClosedOrderIdeal X)

Closed order ideals of a Banach lattice form a lattice under inclusion, with binary meets given by intersection and binary joins by the sum.

Equations

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

@[instance_reducible]

instance ClosedOrderIdeal.instInfSet {X : Type u_2} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] : InfSet (ClosedOrderIdeal X)

Closed order ideals of a Banach lattice admit arbitrary intersections: they form a complete semilattice for the ⊓ operation.

Equations

• ClosedOrderIdeal.instInfSet = { sInf := ClosedOrderIdeal.sInf }

@[simp]

theorem ClosedOrderIdeal.mem_sInf {X : Type u_2} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] {S : Set (ClosedOrderIdeal X)} {x : X} : x ∈ InfSet.sInf S ↔ ∀ J ∈ S, x ∈ J

Membership in an arbitrary intersection of closed order ideals.

@[simp]

theorem ClosedOrderIdeal.inf_toSubmodule {X : Type u_2} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] (J₁ J₂ : ClosedOrderIdeal X) : (J₁ ⊓ J₂).toSubmodule = J₁.toSubmodule ⊓ J₂.toSubmodule

The underlying submodule of a binary meet is the intersection of the underlying submodules.

@[simp]

theorem ClosedOrderIdeal.sup_toSubmodule {X : Type u_2} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] (J₁ J₂ : ClosedOrderIdeal X) : (J₁ ⊔ J₂).toSubmodule = J₁.toSubmodule + J₂.toSubmodule

The underlying submodule of a binary join is the sum of the underlying submodules.