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