Theorems · Theorem · Lie groups

exists_idempotent_in_compact_subsemigroup

∀ {M : Type u_1} [inst : Semigroup M] [inst_1 : TopologicalSpace M] [T2Space M],
  (∀ (r : M), Continuous fun x => x * r) →
    ∀ (s : Set M), s.Nonempty → IsCompact s → (∀ x ∈ s, ∀ y ∈ s, x * y ∈ s) → ∃ 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.

Defined in

Mathlib.Topology.Algebra.Semigroup

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemigroupTopologicalSpaceT2Space