Papers With

← All papers
First page of Effros' theorem on transitive group actions with a glimpse into descriptive set theory

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

Jochen Wengenroth

math.FA Nov 30, 2025 · v1
formalization topology logic
Read PDF arXiv abstract
TL;DR
A non-metrizable version of Effros' theorem on transitive group actions was formalized and verified in Lean by Lara Toledano.
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.
Problem

Effros' theorem on transitive group actions is a fundamental result in descriptive set theory, but existing proofs either assume metrizability or are not fully self-contained. A formal verification of the non-metrizable generalization is lacking.

Approach

The authors prove a version of Effros' theorem about transitive group actions in a non-metrizable setting, following a proof close to van Mill's approach. The presentation is self-contained and covers results about Suslin spaces (continuous images of separable completely metrizable spaces). The proof has been formalized and verified in Lean by Lara Toledano.

Results

A non-metrizable version of Effros' theorem is proved and formally verified in Lean. The paper also establishes several auxiliary results about Suslin spaces, the Borel sigma-algebra, and open mapping theorems that serve as building blocks.