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.

instance ContinuousMap.instIsOrderedMonoid {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [PartialOrder β] [CommMonoid β] [IsOrderedMonoid β] [ContinuousMul β] : IsOrderedMonoid C(α, β)

instance ContinuousMap.instIsOrderedAddMonoid {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [PartialOrder β] [AddCommMonoid β] [IsOrderedAddMonoid β] [ContinuousAdd β] : IsOrderedAddMonoid C(α, β)

@[simp]

theorem ContinuousMap.coe_mabs {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [Group β] [IsTopologicalGroup β] [Lattice β] [TopologicalLattice β] (f : C(α, β)) : ⇑|f|ₘ = |⇑f|ₘ

@[simp]

theorem ContinuousMap.coe_abs {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [AddGroup β] [IsTopologicalAddGroup β] [Lattice β] [TopologicalLattice β] (f : C(α, β)) : ⇑|f| = |⇑f|

@[simp]

theorem ContinuousMap.mabs_apply {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [Group β] [IsTopologicalGroup β] [Lattice β] [TopologicalLattice β] (f : C(α, β)) (x : α) : |f|ₘ x = |f x|ₘ

@[simp]

theorem ContinuousMap.abs_apply {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [AddGroup β] [IsTopologicalAddGroup β] [Lattice β] [TopologicalLattice β] (f : C(α, β)) (x : α) : |f| x = |f x|