# Topology on a linear ordered commutative group #

In this file we prove that a linear ordered commutative group with order topology is a topological group. We also prove continuity of `abs : G → G` and provide convenience lemmas like `ContinuousAt.abs`.

source
@[instance 100]
instance LinearOrderedCommGroup.toIsTopologicalGroup {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] :
IsTopologicalGroup G
source
@[instance 100]
instance LinearOrderedAddCommGroup.toIsTopologicalAddGroup {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] :
IsTopologicalAddGroup G
source
theorem continuous_mabs {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] :
Continuous mabs
source
theorem continuous_abs {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] :
Continuous abs
source
theorem Filter.Tendsto.mabs {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] {α : Type u_2} {l : Filter α} {f : α → G} {a : G} (h : Tendsto f l (nhds a)) :
Tendsto (fun (x : α) => |f x|ₘ) l (nhds |a|ₘ)
source
theorem Filter.Tendsto.abs {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] {α : Type u_2} {l : Filter α} {f : α → G} {a : G} (h : Tendsto f l (nhds a)) :
Tendsto (fun (x : α) => |f x|) l (nhds |a|)
source
@[simp]
theorem comap_mabs_nhds_one {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] :
Filter.comap mabs (nhds 1) = nhds 1
source
@[simp]
theorem comap_abs_nhds_zero {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] :
Filter.comap abs (nhds 0) = nhds 0
source
theorem tendsto_one_iff_mabs_tendsto_one {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] {α : Type u_2} {l : Filter α} (f : α → G) :
Filter.Tendsto f l (nhds 1) ↔ Filter.Tendsto (mabs ∘ f) l (nhds 1)
source
theorem tendsto_zero_iff_abs_tendsto_zero {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] {α : Type u_2} {l : Filter α} (f : α → G) :
Filter.Tendsto f l (nhds 0) ↔ Filter.Tendsto (abs ∘ f) l (nhds 0)
source
theorem Continuous.mabs {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] {X : Type u_2} [TopologicalSpace X] {f : X → G} (h : Continuous f) :
Continuous fun (x : X) => |f x|ₘ
source
theorem Continuous.abs {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] {X : Type u_2} [TopologicalSpace X] {f : X → G} (h : Continuous f) :
Continuous fun (x : X) => |f x|
source
theorem ContinuousAt.mabs {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] {X : Type u_2} [TopologicalSpace X] {f : X → G} {x : X} (h : ContinuousAt f x) :
ContinuousAt (fun (x : X) => |f x|ₘ) x
source
theorem ContinuousAt.abs {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] {X : Type u_2} [TopologicalSpace X] {f : X → G} {x : X} (h : ContinuousAt f x) :
ContinuousAt (fun (x : X) => |f x|) x
source
theorem ContinuousWithinAt.mabs {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] {X : Type u_2} [TopologicalSpace X] {f : X → G} {s : Set X} {x : X} (h : ContinuousWithinAt f s x) :
ContinuousWithinAt (fun (x : X) => |f x|ₘ) s x
source
theorem ContinuousWithinAt.abs {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] {X : Type u_2} [TopologicalSpace X] {f : X → G} {s : Set X} {x : X} (h : ContinuousWithinAt f s x) :
ContinuousWithinAt (fun (x : X) => |f x|) s x
source
theorem ContinuousOn.mabs {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] {X : Type u_2} [TopologicalSpace X] {f : X → G} {s : Set X} (h : ContinuousOn f s) :
ContinuousOn (fun (x : X) => |f x|ₘ) s
source
theorem ContinuousOn.abs {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] {X : Type u_2} [TopologicalSpace X] {f : X → G} {s : Set X} (h : ContinuousOn f s) :
ContinuousOn (fun (x : X) => |f x|) s
source
theorem tendsto_mabs_nhdsNE_one {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] :
Filter.Tendsto mabs (nhdsWithin 1 {1}ᶜ) (nhdsWithin 1 (Set.Ioi 1))
source
theorem tendsto_abs_nhdsNE_zero {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] :
Filter.Tendsto abs (nhdsWithin 0 {0}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
source
theorem denseRange_zpow_iff_surjective {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] {a : G} :
(DenseRange fun (x : ℤ) => a ^ x) ↔ Function.Surjective fun (x : ℤ) => a ^ x

In a linearly ordered multiplicative group, the integer powers of an element are dense iff they are the whole group.

source
theorem denseRange_zsmul_iff_surjective {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] {a : G} :
(DenseRange fun (x : ℤ) => x • a) ↔ Function.Surjective fun (x : ℤ) => x • a

In a linearly ordered additive group, the integer multiples of an element are dense iff they are the whole group.

source
theorem not_denseRange_zpow {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] [Nontrivial G] [DenselyOrdered G] {a : G} :
¬DenseRange fun (x : ℤ) => a ^ x

In a nontrivial densely linearly ordered commutative group, the integer powers of an element can't be dense.

source
theorem not_denseRange_zsmul {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] [Nontrivial G] [DenselyOrdered G] {a : G} :
¬DenseRange fun (x : ℤ) => x • a

In a nontrivial densely linearly ordered additive group, the integer multiples of an element can't be dense.