Theorems · Theorem · Lie groups

exists_idempotent_in_compact_add_subsemigroup

∀ {M : Type u_1} [inst : AddSemigroup 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_add_left where the idempotent lies in some specified nonempty compact additive 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

AddSemigroupTopologicalSpaceT2Space