C(K, ℝ) as a Banach lattice

For a compact topological space K, the space C(K, ℝ) of continuous real-valued functions equipped with the supremum norm and the pointwise order is a Banach lattice.

Lattice and order structure

Mathlib provides Lattice C(K, ℝ) (pointwise, via ContinuousMap.instLatticeOfTopologicalLattice) and IsOrderedAddMonoid C(K, ℝ) (via ContinuousMap.instIsOrderedAddMonoid). The norm comes from ContinuousMap.instNormedAddCommGroup.

Vector lattice

@[instance_reducible]

noncomputable instance instVectorLatticeCofK {K : Type u_1} [TopologicalSpace K] : VectorLattice C(K, ℝ)

C(K, ℝ) is a vector lattice: a real module whose positive cone is closed under scalar multiplication by non-negative reals.

Equations

• instVectorLatticeCofK = { toModule := ContinuousMap.module, toPosSMulMono := ⋯ }

Normed vector lattice

instance instHasSolidNormCofK {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : HasSolidNorm C(K, ℝ)

The sup norm on C(K, ℝ) is solid: |f| ≤ |g| pointwise implies ‖f‖ ≤ ‖g‖.

@[instance_reducible]

noncomputable instance instNormedVectorLatticeCofK {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedVectorLattice C(K, ℝ)

C(K, ℝ) is a normed vector lattice.

Equations

• instNormedVectorLatticeCofK = { toVectorLattice := instVectorLatticeCofK, toHasSolidNorm := ⋯, toNormSMulClass := ⋯ }

Banach lattice

@[instance_reducible]

noncomputable instance instBanachLatticeCofK {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : BanachLattice C(K, ℝ)

C(K, ℝ) is a Banach lattice: a complete normed vector lattice.

Equations

• instBanachLatticeCofK = { toNormedVectorLattice := instNormedVectorLatticeCofK, toCompleteSpace := ⋯ }