Commit 2025-12-02 15:26 f7cf1b32
View on Github →feat(Topology): IsCompletelyPseudoMetrizable (#31235) Introduce the notion of IsCompletelyPseudoMetrizable. The main motivation is to prove the first Baire theorem for a completely pseudometrizable space. Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/First.20Baire.20theorem