instance CofK.instLattice {K : Type u_1} [TopologicalSpace K] : Lattice C(K, ℝ)

Equations

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

instance CofK.instIsOrderedAddMonoid {K : Type u_1} [TopologicalSpace K] : IsOrderedAddMonoid C(K, ℝ)

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

Equations

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