# 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 : M) => x + r) :
∃ (m : 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 : M) => x * r) :
∃ (m : 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 : M) => x + r) (s : Set M) (snemp : s.Nonempty) (s_compact : ) (s_add : xs, ys, x + y s) :
ms, 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 : M) => x * r) (s : Set M) (snemp : s.Nonempty) (s_compact : ) (s_add : xs, ys, x * y s) :
ms, 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.