Semigroup

📁 Source: Mathlib/Topology/Algebra/Semigroup.lean

Statistics

Metric	Count
Definitions Semigroup	1
Theorems exists_idempotent_in_compact_add_subsemigroup, exists_idempotent_in_compact_subsemigroup, exists_idempotent_of_compact_t2_of_continuous_add_left, exists_idempotent_of_compact_t2_of_continuous_mul_left	4
Total	5

(root)

Definitions

Name	Category	Theorems
Semigroup 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_idempotent_in_compact_add_subsemigroup 📖	—	Continuous AddSemigroup.toAdd Set.Nonempty IsCompact Set Set.instMembership	—	—	add_assoc Continuous.comp continuous_subtype_val exists_idempotent_of_compact_t2_of_continuous_add_left nonempty_subtype isCompact_iff_compactSpace instT2SpaceSubtype
exists_idempotent_in_compact_subsemigroup 📖	—	Continuous Semigroup.toMul Set.Nonempty IsCompact Set Set.instMembership	—	—	mul_assoc Continuous.comp continuous_subtype_val exists_idempotent_of_compact_t2_of_continuous_mul_left nonempty_subtype isCompact_iff_compactSpace instT2SpaceSubtype
exists_idempotent_of_compact_t2_of_continuous_add_left 📖	—	Continuous AddSemigroup.toAdd	—	—	zorn_superset isClosed_sInter Set.eq_empty_or_nonempty Set.sInter_empty Set.univ_nonempty Set.sInter_eq_iInter IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed Set.Nonempty.coe_sort DirectedOn.directed_val IsChain.directedOn instReflGe IsChain.symm Subtype.prop IsClosed.isCompact Set.mem_sInter Set.sInter_subset_of_mem Minimal.prop Minimal.eq_of_subset Continuous.isClosedMap add_assoc IsClosed.inter IsClosed.preimage T1Space.t1 T2Space.t1Space Set.mem_setOf_eq Set.inter_subset_left
exists_idempotent_of_compact_t2_of_continuous_mul_left 📖	—	Continuous Semigroup.toMul	—	—	zorn_superset isClosed_sInter Set.eq_empty_or_nonempty Set.sInter_empty Set.univ_nonempty Set.sInter_eq_iInter IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed Set.Nonempty.coe_sort DirectedOn.directed_val IsChain.directedOn instReflGe IsChain.symm Subtype.prop IsClosed.isCompact Set.mem_sInter Set.sInter_subset_of_mem Minimal.prop Minimal.eq_of_subset Continuous.isClosedMap mul_assoc IsClosed.inter IsClosed.preimage T1Space.t1 T2Space.t1Space Set.mem_setOf_eq Set.inter_subset_left

---

← Back to Index