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]
def
linear_ordered_add_comm_group.topological_add_group
{G : Type u_2}
[topological_space G]
[linear_ordered_add_comm_group G]
[order_topology G] :
@[continuity]
theorem
continuous_abs
{G : Type u_2}
[topological_space G]
[linear_ordered_add_comm_group G]
[order_topology G] :
@[protected]
theorem
filter.tendsto.abs
{α : Type u_1}
{G : Type u_2}
[topological_space G]
[linear_ordered_add_comm_group G]
[order_topology G]
{l : filter α}
{f : α → G}
{a : G}
(h : filter.tendsto f l (nhds a)) :
theorem
tendsto_zero_iff_abs_tendsto_zero
{α : Type u_1}
{G : Type u_2}
[topological_space G]
[linear_ordered_add_comm_group G]
[order_topology G]
{l : filter α}
(f : α → G) :
filter.tendsto f l (nhds 0) ↔ filter.tendsto (has_abs.abs ∘ f) l (nhds 0)
@[protected]
theorem
continuous.abs
{α : Type u_1}
{G : Type u_2}
[topological_space G]
[linear_ordered_add_comm_group G]
[order_topology G]
{f : α → G}
[topological_space α]
(h : continuous f) :
continuous (λ (x : α), |f x|)
@[protected]
theorem
continuous_at.abs
{α : Type u_1}
{G : Type u_2}
[topological_space G]
[linear_ordered_add_comm_group G]
[order_topology G]
{f : α → G}
[topological_space α]
{a : α}
(h : continuous_at f a) :
continuous_at (λ (x : α), |f x|) a
@[protected]
theorem
continuous_within_at.abs
{α : Type u_1}
{G : Type u_2}
[topological_space G]
[linear_ordered_add_comm_group G]
[order_topology G]
{f : α → G}
[topological_space α]
{a : α}
{s : set α}
(h : continuous_within_at f s a) :
continuous_within_at (λ (x : α), |f x|) s a
@[protected]
theorem
continuous_on.abs
{α : Type u_1}
{G : Type u_2}
[topological_space G]
[linear_ordered_add_comm_group G]
[order_topology G]
{f : α → G}
[topological_space α]
{s : set α}
(h : continuous_on f s) :
continuous_on (λ (x : α), |f x|) s
theorem
tendsto_abs_nhds_within_zero
{G : Type u_2}
[topological_space G]
[linear_ordered_add_comm_group G]
[order_topology G] :
filter.tendsto has_abs.abs (nhds_within 0 {0}ᶜ) (nhds_within 0 (set.Ioi 0))