exists_idempotent_of_compact_t2_of_continuous_mul_left
theorem exists_idempotent_of_compact_t2_of_continuous_mul_left :
∀ {M : Type u_1} [inst : Nonempty M] [inst : Semigroup M] [inst_1 : TopologicalSpace M] [inst_2 : CompactSpace M]
[inst_3 : T2Space M], (∀ (r : M), Continuous fun x => x * r) → ∃ m, m * m = m
This theorem states that for any nonempty semigroup `M` equipped with a topology such that `M` is compact and Hausdorff (or T2), if the operation of right-multiplication by any element is a continuous function, then there exists an idempotent element `m` in `M`. An element is called idempotent if it satisfies the condition `m * m = m`.
More concisely: In a compact and Hausdorff semigroup endowed with a topology where right-multiplication by any element is a continuous function, there exists an idempotent element.
|
exists_idempotent_in_compact_subsemigroup
theorem exists_idempotent_in_compact_subsemigroup :
∀ {M : Type u_1} [inst : Semigroup M] [inst_1 : TopologicalSpace M] [inst_2 : 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
This theorem, called `exists_idempotent_in_compact_subsemigroup`, asserts that for a given type `M` with a semigroup structure and a T2 (or "Hausdorff") topological space structure, if the left multiplication operation is continuous, then for any set `s` in `M` that is nonempty and compact and closed under the semigroup operation, there exists an idempotent element `m` in `s`. An idempotent element is one for which squaring the element (i.e., applying the semigroup operation to the element and itself) results in the element itself (in other words, `m * m = m`).
More concisely: Given a compact and nonempty semigroup `M` with a T2 topology and a continuous left multiplication operation, there exists an idempotent element in `M`.
|
exists_idempotent_of_compact_t2_of_continuous_add_left
theorem exists_idempotent_of_compact_t2_of_continuous_add_left :
∀ {M : Type u_1} [inst : Nonempty M] [inst : AddSemigroup M] [inst_1 : TopologicalSpace M] [inst_2 : CompactSpace M]
[inst_3 : T2Space M], (∀ (r : M), Continuous fun x => x + r) → ∃ m, m + m = m
This theorem states that in any nonempty compact Hausdorff (T2) additive semigroup, if right-addition is a continuous operation, then there exists an idempotent element. An idempotent element is an element `m` such that when it is added to itself (i.e., `m + m`), it results in `m` again. In other words, there is an element in the semigroup which remains unchanged when added to itself, under the conditions that the semigroup is nonempty, compact, Hausdorff and right-addition is continuous.
More concisely: In a nonempty, compact Hausdorff additive semigroup where right-addition is continuous, there exists an idempotent element.
|
exists_idempotent_in_compact_add_subsemigroup
theorem exists_idempotent_in_compact_add_subsemigroup :
∀ {M : Type u_1} [inst : AddSemigroup M] [inst_1 : TopologicalSpace M] [inst_2 : 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
The theorem `exists_idempotent_in_compact_add_subsemigroup` states that for any type `M` that has the structure of an additive semigroup and a T2 topological space, and for which addition of any element `r` is a continuous function, if `s` is a non-empty compact set within `M` that forms an additive subsemigroup (i.e., the sum of any two elements of `s` is still in `s`), then there exists an element `m` within `s` that is idempotent with respect to addition, meaning `m + m = m`.
More concisely: Given a T2 topological space `M` equipped with the structure of a compact, non-empty additive semigroup where addition of any element is continuous, there exists an idempotent element in `M`.
|