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]
instance
LinearOrderedAddCommGroup.topologicalAddGroup
{G : Type u_2}
[TopologicalSpace G]
[LinearOrderedAddCommGroup G]
[OrderTopology G]
:
Equations
- ⋯ = ⋯
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))
theorem
denseRange_zsmul_iff_surjective
{G : Type u_2}
[TopologicalSpace G]
[LinearOrderedAddCommGroup G]
[OrderTopology G]
{a : G}
:
(DenseRange fun (x : ℤ) => x • a) ↔ Function.Surjective fun (x : ℤ) => x • a
In a linearly ordered additive group, the integer multiples of an element are dense iff they are the whole group.
theorem
not_denseRange_zsmul
{G : Type u_2}
[TopologicalSpace G]
[LinearOrderedAddCommGroup G]
[OrderTopology G]
[Nontrivial G]
[DenselyOrdered G]
{a : G}
:
¬DenseRange fun (x : ℤ) => x • a
In a nontrivial densely linearly ordered additive group, the integer multiples of an element can't be dense.