# Documentation

Mathlib.Topology.Algebra.Semigroup

# Idempotents in topological semigroups #

This file provides a sufficient condition for a semigroup M to contain an idempotent (i.e. an element m such that m * m = m ), namely that M is a nonempty compact Hausdorff space where right-multiplication by constants is continuous.

We also state a corresponding lemma guaranteeing that a subset of M contains an idempotent.

theorem exists_idempotent_of_compact_t2_of_continuous_add_left {M : Type u_1} [] [] [] [] [] (continuous_mul_left : ∀ (r : M), Continuous fun x => x + r) :
m, m + m = m

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

theorem exists_idempotent_of_compact_t2_of_continuous_mul_left {M : Type u_1} [] [] [] [] [] (continuous_mul_left : ∀ (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.

theorem exists_idempotent_in_compact_add_subsemigroup {M : Type u_1} [] [] [] (continuous_mul_left : ∀ (r : M), Continuous fun x => x + r) (s : Set M) (snemp : ) (s_compact : ) (s_add : ∀ (x : M), x s∀ (y : M), y sx + y s) :
m, m s m + m = m

A version of exists_idempotent_of_compact_t2_of_continuous_add_left where the idempotent lies in some specified nonempty compact additive subsemigroup.

theorem exists_idempotent_in_compact_subsemigroup {M : Type u_1} [] [] [] (continuous_mul_left : ∀ (r : M), Continuous fun x => x * r) (s : Set M) (snemp : ) (s_compact : ) (s_add : ∀ (x : M), x s∀ (y : M), y sx * y s) :
m, m s m * m = m

A version of exists_idempotent_of_compact_t2_of_continuous_mul_left where the idempotent lies in some specified nonempty compact subsemigroup.