# mathlib3documentation

topology.algebra.order.group

# Topology on a linear ordered additive commutative group #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 continuous_at.abs.

@[protected, instance]
@[continuity]
theorem continuous_abs {G : Type u_2}  :
@[protected]
theorem filter.tendsto.abs {α : Type u_1} {G : Type u_2} {l : filter α} {f : α G} {a : G} (h : (nhds a)) :
filter.tendsto (λ (x : α), |f x|) l (nhds |a|)
theorem tendsto_zero_iff_abs_tendsto_zero {α : Type u_1} {G : Type u_2} {l : filter α} (f : α G) :
(nhds 0) l (nhds 0)
@[protected]
theorem continuous.abs {α : Type u_1} {G : Type u_2} {f : α G} (h : continuous f) :
continuous (λ (x : α), |f x|)
@[protected]
theorem continuous_at.abs {α : Type u_1} {G : Type u_2} {f : α G} {a : α} (h : a) :
continuous_at (λ (x : α), |f x|) a
@[protected]
theorem continuous_within_at.abs {α : Type u_1} {G : Type u_2} {f : α G} {a : α} {s : set α} (h : a) :
continuous_within_at (λ (x : α), |f x|) s a
@[protected]
theorem continuous_on.abs {α : Type u_1} {G : Type u_2} {f : α G} {s : set α} (h : s) :
continuous_on (λ (x : α), |f x|) s
theorem tendsto_abs_nhds_within_zero {G : Type u_2}  :
(set.Ioi 0))