Theorems · Theorem · Lie groups

IsTopologicalGroup.of_comm_of_nhds_one

∀ {G : Type u} [inst : CommGroup G] [inst_1 : TopologicalSpace G],
  Filter.Tendsto (Function.uncurry fun x1 x2 => x1 * x2) (nhds 1 ×ˢ nhds 1) (nhds 1) →
    Filter.Tendsto (fun x => x⁻¹) (nhds 1) (nhds 1) →
      (∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ * x) (nhds 1)) → IsTopologicalGroup G

Defined in

Mathlib.Topology.Algebra.Group.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommGroupTopologicalSpace