Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-03-11 14:26 64a8d564

View on Github →

chore(order/filter): simplify definition of filter.prod; cleanup

Estimated changes

Modified analysis/ennreal.lean

Modified analysis/real.lean

Modified analysis/topology/continuity.lean

Modified analysis/topology/topological_space.lean

added theorem nhds_sup

Modified analysis/topology/uniform_space.lean

modified theorem uniformity_le_symm

Modified data/analysis/filter.lean

Modified order/filter.lean

added theorem filter.le_lift

added theorem filter.lift_const

added theorem filter.lift_inf

added theorem filter.lift_principal2

modified theorem filter.map_lift_eq

added theorem filter.map_swap_eq_vmap_swap

deleted theorem filter.map_swap_vmap_swap_eq

added theorem filter.mem_prod_iff

deleted theorem filter.mem_prod_sets

added theorem filter.prod_bot1

added theorem filter.prod_bot2

added theorem filter.prod_comm'

modified theorem filter.prod_def

modified theorem filter.prod_mem_prod

modified theorem filter.prod_neq_bot

modified theorem filter.prod_principal_principal

modified theorem filter.vmap_lift_eq