Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-24 20:37 0d16bb4d

View on Github →

refactor(*): migrate from filter.lift' _ powerset to filter.small_sets (#13673)

Estimated changes

deleted theorem filter.lift'_inf_powerset
modified theorem filter.has_basis.small_sets
modified theorem filter.has_basis_small_sets
modified def filter.small_sets
added theorem filter.small_sets_bot
added theorem filter.small_sets_inf
added theorem filter.small_sets_infi
added theorem filter.small_sets_top
modified theorem bsupr_limsup_dimH
modified theorem supr_limsup_dimH