α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f✝ g f : α → G
h : Tendsto (abs ∘ f) l (𝓝 0)
⊢ Tendsto f l (𝓝 0)
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f✝ g f : α → G
⊢ Tendsto f l (𝓝 0) ↔ Tendsto (abs ∘ f) l (𝓝 0)
refine' ⟨fun h => (abs_zero : |(0 : G)| = 0) ▸ h.abs, fun h => _⟩
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f✝ g f : α → G
h : Tendsto (abs ∘ f) l (𝓝 0)
this : Tendsto (fun a => -abs (f a)) l (𝓝 0)
⊢ Tendsto f l (𝓝 0)
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f✝ g f : α → G
h : Tendsto (abs ∘ f) l (𝓝 0)
⊢ Tendsto f l (𝓝 0)
have : Tendsto (fun a => -|f a|) l (𝓝 0) := (neg_zero : -(0 : G) = 0) ▸ h.neg
no goals
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f✝ g f : α → G
h : Tendsto (abs ∘ f) l (𝓝 0)
this : Tendsto (fun a => -abs (f a)) l (𝓝 0)
⊢ Tendsto f l (𝓝 0)
exact
  tendsto_of_tendsto_of_tendsto_of_le_of_le this h (fun x => neg_abs_le_self <| f x) fun x =>
    le_abs_self <| f x