Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2512.00910 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912738404466688 |
|---|---|
| author | Wengenroth, Jochen |
| author_facet | Wengenroth, Jochen |
| contents | The main aim of this note is to prove a version of a celebrated theorem of Effros about transitive group actions in a non-metrizable setting, these parts have been formalized and verified with Lean by Lara Toledano. We do not claim any originality since the given proof is in fact very close to one of van Mill. Our presentation is however completely self-contained and may serve as an appetizer to descriptive set theory. It also contains a few results about Suslin spaces (continuous images of separable completely metrizable spaces, which are often called analytic) which are extremely useful in measure theory. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_00910 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Effros' theorem on transitive group actions with a glimpse into descriptive set theory Wengenroth, Jochen Functional Analysis Logic 54H05, 22F05 The main aim of this note is to prove a version of a celebrated theorem of Effros about transitive group actions in a non-metrizable setting, these parts have been formalized and verified with Lean by Lara Toledano. We do not claim any originality since the given proof is in fact very close to one of van Mill. Our presentation is however completely self-contained and may serve as an appetizer to descriptive set theory. It also contains a few results about Suslin spaces (continuous images of separable completely metrizable spaces, which are often called analytic) which are extremely useful in measure theory. |
| title | Effros' theorem on transitive group actions with a glimpse into descriptive set theory |
| topic | Functional Analysis Logic 54H05, 22F05 |
| url | https://arxiv.org/abs/2512.00910 |