Theorems · Theorem · Lie groups

Filter.Tendsto.inv

∀ {G : Type u_1} {α : Type u_2} [inst : TopologicalSpace G] [inst_1 : Inv G] [ContinuousInv G] {f : α → G}
  {l : Filter α} {y : G}, Filter.Tendsto f l (nhds y) → Filter.Tendsto (fun x => (f x)⁻¹) l (nhds y⁻¹)

If a function converges to a value in a multiplicative topological group, then its inverse converges to the inverse of this value. For the version in topological groups with zero (including topological fields) assuming additionally that the limit is nonzero, use Filter.Tendsto.inv₀.

Defined in

Mathlib.Topology.Algebra.Group.Defs

Cited by

7 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpaceInvContinuousInv