Commit 2026-01-07 10:31 ff246d7e

feat: a dense Gdelta subset of a Baire space is Baire. (#32674) This PR formalizes:

1. If s is dense in X and u is open and dense in s, then u = v ∩ s for some v that is open and dense in X. We then use this lemma to prove that a dense Gδ subset of a Baire space is Baire.
2. A Gδ subset of a locally compact R1 space is Baire. Formalized with help from Aristotle.