Revision #3138 → #3224 · back to history
1579bf098242| Field | From #3138 | To #3224 |
|---|---|---|
| mathlib.decl | cantorSpace | — |
| note | Mathlib has Cantor space as ℕ → Bool / ℕ → Fin 2 via the standard product topology, but no first-class `BaireSpace = ℕ → ℕ` definition tied to descriptive set theory. | Mathlib has Cantor space as ℕ → Bool / ℕ → Fin 2 via the standard product topology, but no first-class `BaireSpace = ℕ → ℕ` definition tied to descriptive set theory. (Cited declaration no longer exists in Mathlib — cleared by the decl-existence sweep.) |
| provenance | ai | ai-moderated |
| status | partial | not_formalized |