Topology on a linear ordered additive commutative group

In this file we prove that a linear ordered additive 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 LinearOrderedAddCommGroup.topologicalAddGroup {G : Type u_2} [TopologicalSpace G] [LinearOrderedAddCommGroup G] [OrderTopology G] : TopologicalAddGroup G

theorem continuous_abs {G : Type u_2} [TopologicalSpace G] [LinearOrderedAddCommGroup G] [OrderTopology G] : Continuous abs

theorem Filter.Tendsto.abs {α : Type u_1} {G : Type u_2} [TopologicalSpace G] [LinearOrderedAddCommGroup G] [OrderTopology G] {l : Filter α} {f : α → G} {a : G} (h : Filter.Tendsto f l (nhds a)) : Filter.Tendsto (fun (x : α) => |f x|) l (nhds |a|)

theorem tendsto_zero_iff_abs_tendsto_zero {α : Type u_1} {G : Type u_2} [TopologicalSpace G] [LinearOrderedAddCommGroup G] [OrderTopology G] {l : Filter α} (f : α → G) : Filter.Tendsto f l (nhds 0) ↔ Filter.Tendsto (abs ∘ f) l (nhds 0)

theorem Continuous.abs {α : Type u_1} {G : Type u_2} [TopologicalSpace G] [LinearOrderedAddCommGroup G] [OrderTopology G] {f : α → G} [TopologicalSpace α] (h : Continuous f) : Continuous fun (x : α) => |f x|

theorem ContinuousAt.abs {α : Type u_1} {G : Type u_2} [TopologicalSpace G] [LinearOrderedAddCommGroup G] [OrderTopology G] {f : α → G} [TopologicalSpace α] {a : α} (h : ContinuousAt f a) : ContinuousAt (fun (x : α) => |f x|) a

theorem ContinuousWithinAt.abs {α : Type u_1} {G : Type u_2} [TopologicalSpace G] [LinearOrderedAddCommGroup G] [OrderTopology G] {f : α → G} [TopologicalSpace α] {a : α} {s : Set α} (h : ContinuousWithinAt f s a) : ContinuousWithinAt (fun (x : α) => |f x|) s a

theorem ContinuousOn.abs {α : Type u_1} {G : Type u_2} [TopologicalSpace G] [LinearOrderedAddCommGroup G] [OrderTopology G] {f : α → G} [TopologicalSpace α] {s : Set α} (h : ContinuousOn f s) : ContinuousOn (fun (x : α) => |f x|) s

theorem tendsto_abs_nhdsWithin_zero {G : Type u_2} [TopologicalSpace G] [LinearOrderedAddCommGroup G] [OrderTopology G] : Filter.Tendsto abs (nhdsWithin 0 {0}ᶜ) (nhdsWithin 0 (Set.Ioi 0))

theorem denseRange_zsmul_iff_surjective {G : Type u_2} [TopologicalSpace G] [LinearOrderedAddCommGroup 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_zsmul {G : Type u_2} [TopologicalSpace G] [LinearOrderedAddCommGroup 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.