Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-18 12:55 a423cc75

View on Github →

refactor(order/filter): simplify filter structure

Estimated changes

Modified analysis/ennreal.lean

Modified analysis/real.lean

Modified analysis/topology/continuity.lean

Modified analysis/topology/topological_space.lean

Modified analysis/topology/topological_structures.lean

Modified analysis/topology/uniform_space.lean

Modified data/analysis/filter.lean

Modified order/filter.lean

deleted theorem filter.filter.ext

modified theorem filter.inter_mem_sets

added theorem filter.mem_sets_of_superset

modified structure filter

Modified order/liminf_limsup.lean