Theorems · Theorem · Lie groups

tendsto_sub_nhds_zero_iff

∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {α : Type u_1} {l : Filter α}
  {x : G} {u : α → G}, Filter.Tendsto (fun x_1 => u x_1 - x) l (nhds 0) ↔ Filter.Tendsto u l (nhds x)

Defined in

Mathlib.Topology.Algebra.Group.Basic

Cited by

12 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupTopologicalSpaceIsTopologicalAddGroup