English
There exists an idempotent in a nonempty compact subsemigroup s of M.
Русский
Существование идемпотента в заданной непустой компактной подполугруппе s.
LaTeX
$$$\exists m \in s, m^2 = m.$$$
Lean4
/-- A version of `exists_idempotent_of_compact_t2_of_continuous_mul_left` where the idempotent lies
in some specified nonempty compact subsemigroup. -/
@[to_additive exists_idempotent_in_compact_add_subsemigroup /-- 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} [Semigroup M] [TopologicalSpace M] [T2Space M]
(continuous_mul_left : ∀ r : M, Continuous (· * r)) (s : Set M) (snemp : s.Nonempty) (s_compact : IsCompact s)
(s_add : ∀ᵉ (x ∈ s) (y ∈ s), x * y ∈ s) : ∃ m ∈ s, m * m = m :=
by
let M' := { m // m ∈ s }
letI : Semigroup M' :=
{ mul := fun p q => ⟨p.1 * q.1, s_add _ p.2 _ q.2⟩
mul_assoc := fun p q r => Subtype.eq (mul_assoc _ _ _) }
haveI : CompactSpace M' := isCompact_iff_compactSpace.mp s_compact
haveI : Nonempty M' := nonempty_subtype.mpr snemp
have : ∀ p : M', Continuous (· * p) := fun p => ((continuous_mul_left p.1).comp continuous_subtype_val).subtype_mk _
obtain ⟨⟨m, hm⟩, idem⟩ := exists_idempotent_of_compact_t2_of_continuous_mul_left this
exact ⟨m, hm, Subtype.ext_iff.mp idem⟩
