Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-27 02:48 d6e399f1

View on Github →

chore(order/filter/basic): add @[simp] to principal_empty/univ (#3572)

Estimated changes

Modified src/order/filter/at_top_bot.lean

Modified src/order/filter/bases.lean

Modified src/order/filter/basic.lean

modified theorem filter.principal_empty

modified theorem filter.principal_univ

Modified src/topology/subset_properties.lean