Documentation

Mathlib.Topology.Algebra.Order.Group

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.

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