Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-13 15:02 95d4f658

View on Github →

refactor(topology/sets/compacts): rename projection to is_compact (#16949) In the structures compacts, nonempty_compacts, compact_opens, positive_compacts rename the field compact to is_compact.

Estimated changes