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

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

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