Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-03-05 18:18 5193194e

View on Github →

feat(order/filter): reorder filter theory; add filter_upwards tactic

Estimated changes

Modified analysis/topology/topological_space.lean

Modified analysis/topology/uniform_space.lean

Modified order/filter.lean

modified theorem filter.Inter_mem_sets

modified theorem filter.exists_sets_subset_iff

modified theorem filter.filter.ext

modified theorem filter.filter_eq_iff

modified theorem filter.inter_mem_sets

modified theorem filter.mem_inf_sets_of_left

modified theorem filter.mem_inf_sets_of_right

added theorem filter.mp_sets

added theorem filter.tendsto_inf_left

added theorem filter.tendsto_inf_right

modified theorem filter.univ_mem_sets'

modified theorem filter.univ_mem_sets