Theorems · Theorem · Lie groups

tendsto_inv_iff

∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [ContinuousInv G] {l : Filter α}
  {m : α → G} {a : G}, Filter.Tendsto (fun x => (m x)⁻¹) l (nhds a⁻¹) ↔ Filter.Tendsto m l (nhds a)

Defined in

Mathlib.Topology.Algebra.Group.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceInvolutiveInvContinuousInv