Theorems · Theorem · Lie groups

exists_idempotent_of_compact_t2_of_continuous_mul_left

∀ {M : Type u_1} [Nonempty M] [inst : Semigroup M] [inst_1 : TopologicalSpace M] [CompactSpace M] [T2Space M],
  (∀ (r : M), Continuous fun x => x * r) → ∃ m, m * m = m

Any nonempty compact Hausdorff semigroup where right-multiplication is continuous contains an idempotent, i.e. an m such that m * m = m.

Defined in

Mathlib.Topology.Algebra.Semigroup

Cited by

2 results in Mathlib

Foundations

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

Assumes

NonemptySemigroupTopologicalSpaceCompactSpaceT2Space