# Continuous maps as a lattice ordered group #

We now provide formulas for `f ⊓ g` and `f ⊔ g`, where `f g : C(α, β)`, in terms of `ContinuousMap.abs`.

`C(α, β)`is a lattice ordered group

source
instance ContinuousMap.instIsOrderedMonoid {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [PartialOrder β] [CommMonoid β] [IsOrderedMonoid β] [ContinuousMul β] :
IsOrderedMonoid C(α, β)
source
instance ContinuousMap.instIsOrderedAddMonoid {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [PartialOrder β] [AddCommMonoid β] [IsOrderedAddMonoid β] [ContinuousAdd β] :
IsOrderedAddMonoid C(α, β)
source
@[simp]
theorem ContinuousMap.coe_mabs {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [Group β] [IsTopologicalGroup β] [Lattice β] [TopologicalLattice β] (f : C(α, β)) :
⇑|f|ₘ = |⇑f|ₘ
source
@[simp]
theorem ContinuousMap.coe_abs {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [AddGroup β] [IsTopologicalAddGroup β] [Lattice β] [TopologicalLattice β] (f : C(α, β)) :
⇑|f| = |⇑f|
source
@[simp]
theorem ContinuousMap.mabs_apply {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [Group β] [IsTopologicalGroup β] [Lattice β] [TopologicalLattice β] (f : C(α, β)) (x : α) :
|f|ₘ x = |f x|ₘ
source
@[simp]
theorem ContinuousMap.abs_apply {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [AddGroup β] [IsTopologicalAddGroup β] [Lattice β] [TopologicalLattice β] (f : C(α, β)) (x : α) :
|f| x = |f x|