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.

@[instance 100]

instance LinearOrderedCommGroup.toIsTopologicalGroup {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] : IsTopologicalGroup G

@[instance 100]

instance LinearOrderedAddCommGroup.toIsTopologicalAddGroup {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] : IsTopologicalAddGroup G

theorem continuous_mabs {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] : Continuous mabs

theorem continuous_abs {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] : Continuous abs

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|ₘ)

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|)

@[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

@[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

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)

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)

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|ₘ

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|

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

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

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

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

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

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

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))

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))

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.

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.

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.

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.