Effros' theorem on transitive group actions with a glimpse into descriptive set theory

TL;DR

This paper presents a formalized version of Effros' theorem for transitive group actions in non-metrizable spaces, connecting group actions with descriptive set theory and measure theory, verified using Lean proof assistant.

Contribution

It provides a self-contained proof of Effros' theorem in a non-metrizable setting and explores properties of Suslin spaces relevant to measure theory.

Findings

Formalized Effros' theorem in Lean

Extended understanding of Suslin spaces in measure theory

Self-contained presentation accessible to descriptive set theory

Abstract

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.