Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-11 19:03 6d907282

View on Github →

use Galois connections in filter library

Estimated changes

added theorem filter.gc_map_vmap
modified theorem filter.image_mem_map
modified theorem filter.le_vmap_map
modified theorem filter.map_bot
modified theorem filter.map_compose
modified theorem filter.map_eq_bot_iff
modified theorem filter.map_id
modified theorem filter.map_map
modified theorem filter.map_mono
modified theorem filter.map_ne_bot
modified theorem filter.map_sup
added theorem filter.map_supr
modified theorem filter.map_vmap_le
modified theorem filter.mem_map
modified theorem filter.mem_vmap
modified theorem filter.monotone_map
modified theorem filter.monotone_vmap
modified theorem filter.preimage_mem_vmap
deleted theorem filter.supr_map
added theorem filter.vmap_id
modified theorem filter.vmap_inf
modified theorem filter.vmap_infi
modified theorem filter.vmap_mono
modified theorem filter.vmap_principal
modified theorem filter.vmap_sup
added theorem filter.vmap_top
modified theorem filter.vmap_vmap_comp