Bands #

A band in a vector lattice is an order ideal that is order closed: whenever a subset of the band has a supremum in the ambient space, that supremum also lies in the band.

This file defines the bundled structure Band, relates bands to order ideals and vector sublattices, proves the basic closure properties, and records that order completeness passes from the ambient vector lattice to a band.

The band structure #

source

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

Type u_2

A band in a vector lattice is an order ideal that is order closed: whenever a subset of the band has a supremum in X, that supremum also lies in the band.

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
sSup_mem' (S : Set X) : S ⊆ self.carrier → S.Nonempty → ∀ (x : X), IsLUB S x → x ∈ self.carrier

Instances For

source

@[instance_reducible]

instance Band.instSetLike {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] :

SetLike (Band X) X

Equations

Band.instSetLike = { coe := fun (B : Band X) => B.carrier, coe_injective := ⋯ }

A band is an ideal and a vector sublattice #

Closure under suprema #

source

theorem Band.sSup_mem {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (B : Band X) {S : Set X} (hS : S ⊆ ↑B) (hne : S.Nonempty) {x : X} (hx : IsLUB S x) :

x ∈ B

A band is closed under suprema: if a subset of the band has a supremum in X, the supremum lies in the band.

Basic membership lemmas inherited from the underlying ideal #

source

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

x ⊔ y ∈ B

A band is closed under ⊔.

source

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

x ⊓ y ∈ B

A band is closed under ⊓.

source

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

y ∈ B

A band is solid.

source

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

|x| ∈ B

A band is closed under absolute value.

source

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

x ∈ B

Membership in a band is equivalent to membership of the absolute value.

source

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

y ∈ B

Solidity in terms of absolute value.

Construction from the positive directed closure condition #

It suffices to test the closure condition on positive directed subsets: an order ideal closed under suprema of positive directed subsets is automatically a band.

source