Commit 2025-11-03 01:23 d00cab50

View on Github →

fix(Topology/Baire/Lemmas): fix index type in isMeagre_iUnion (#30141) The index set ι needs to be of type Sort* instead of type Type* in isMeagre_iUnion otherwise I get the following message when I try to use it: typeclass instance problem is stuck, it is often due to metavariables Countable ?m.27

Estimated changes