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.instMulLeftMono
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[TopologicalSpace β]
[PartialOrder β]
[Mul β]
[ContinuousMul β]
[MulLeftMono β]
:
MulLeftMono C(α, β)
instance
ContinuousMap.instAddLeftMono
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[TopologicalSpace β]
[PartialOrder β]
[Add β]
[ContinuousAdd β]
[AddLeftMono β]
:
AddLeftMono C(α, β)
instance
ContinuousMap.instMulRightMono
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[TopologicalSpace β]
[PartialOrder β]
[Mul β]
[ContinuousMul β]
[MulRightMono β]
:
MulRightMono C(α, β)
instance
ContinuousMap.instAddRightMono
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[TopologicalSpace β]
[PartialOrder β]
[Add β]
[ContinuousAdd β]
[AddRightMono β]
:
AddRightMono C(α, β)
@[simp]
theorem
ContinuousMap.coe_mabs
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[TopologicalSpace β]
[Group β]
[TopologicalGroup β]
[Lattice β]
[TopologicalLattice β]
(f : C(α, β))
:
@[simp]
theorem
ContinuousMap.coe_abs
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[TopologicalSpace β]
[AddGroup β]
[TopologicalAddGroup β]
[Lattice β]
[TopologicalLattice β]
(f : C(α, β))
:
⇑|f| = |⇑f|
@[simp]
theorem
ContinuousMap.mabs_apply
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[TopologicalSpace β]
[Group β]
[TopologicalGroup β]
[Lattice β]
[TopologicalLattice β]
(f : C(α, β))
(x : α)
:
@[simp]
theorem
ContinuousMap.abs_apply
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[TopologicalSpace β]
[AddGroup β]
[TopologicalAddGroup β]
[Lattice β]
[TopologicalLattice β]
(f : C(α, β))
(x : α)
:
|f| x = |f x|