Theorems · Theorem · Lie groups

Filter.tendsto_cocompact_mul_right

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

Right-multiplication by a right-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