Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-23 13:44 396a66a0

View on Github →

chore(order/filter/*): use [nonempty _] instead of (_ : nonempty _) (#3526) In most cases Lean can find an instance automatically.

Estimated changes

modified theorem filter.at_top_basis
modified theorem filter.has_basis_generate
modified theorem filter.infi_sets_eq
modified theorem filter.map_infi_eq
modified theorem filter.mem_infi