Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-23 18:58 e2edba53

View on Github →

chore(order/filter/basic): make filter.univ_mem_sets a simp lemma (#5464)

Estimated changes

Modified src/data/list/basic.lean

added theorem list.insert_nth_succ_nil

Modified src/data/rel.lean

modified theorem rel.core_univ

Modified src/order/filter/basic.lean

modified theorem filter.univ_mem_sets

Modified src/order/filter/partial.lean

Modified src/topology/list.lean

modified theorem nhds_nil