# 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]
Equations
• =
theorem continuous_abs {G : Type u_2} [] [] :
theorem Filter.Tendsto.abs {α : Type u_1} {G : Type u_2} [] [] {l : } {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} [] [] {l : } (f : αG) :
theorem Continuous.abs {α : Type u_1} {G : Type u_2} [] [] {f : αG} [] (h : ) :
Continuous fun (x : α) => |f x|
theorem ContinuousAt.abs {α : Type u_1} {G : Type u_2} [] [] {f : αG} [] {a : α} (h : ) :
ContinuousAt (fun (x : α) => |f x|) a
theorem ContinuousWithinAt.abs {α : Type u_1} {G : Type u_2} [] [] {f : αG} [] {a : α} {s : Set α} (h : ) :
ContinuousWithinAt (fun (x : α) => |f x|) s a
theorem ContinuousOn.abs {α : Type u_1} {G : Type u_2} [] [] {f : αG} [] {s : Set α} (h : ) :
ContinuousOn (fun (x : α) => |f x|) s