Theorems · Theorem · general topology

ContinuousMonoidHom.locallyCompactSpace_of_hasBasis

∀ {X : Type u_7} {Y : Type u_8} [inst : TopologicalSpace X] [inst_1 : Group X] [IsTopologicalGroup X]
  [inst_3 : UniformSpace Y] [inst_4 : CommGroup Y] [IsUniformGroup Y] [T0Space Y] [CompactSpace Y]
  [LocallyCompactSpace X] (V : ℕ → Set Y),
  (∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)) →
    (nhds 1).HasBasis (fun x => True) V → LocallyCompactSpace (X →ₜ* Y)

Defined in

Mathlib.Topology.Algebra.Group.CompactOpen

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceGroupIsTopologicalGroupUniformSpaceCommGroupIsUniformGroupT0SpaceCompactSpaceLocallyCompactSpace