Theorems · Theorem · Lie groups

Filter.tendsto_cocompact_mul_left

∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [SeparatelyContinuousMul M] {a b : M},
  b * a = 1 → Filter.Tendsto (fun x => a * x) (Filter.cocompact M) (Filter.cocompact M)

Left-multiplication by a left-invertible element of a topological monoid is proper, i.e., inverse images of compact sets are compact.

Defined in

Mathlib.Topology.Algebra.Monoid

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMonoidSeparatelyContinuousMul