Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-02 22:32 64b61515

View on Github →

refactor(data/set/basic,*): vimage -> preimage, add notation

Estimated changes

modified theorem filter.mem_vmap_of_mem
deleted theorem filter.vimage_mem_vmap
modified theorem filter.vmap_principal
added theorem set.preimage_set_of_eq
added theorem set.prod_preimage_eq
deleted theorem set.prod_vimage_eq
deleted theorem set.vimage_set_of_eq
modified theorem set.image_comp
modified theorem set.image_empty
modified theorem set.image_id
modified theorem set.image_subset
modified def set.mem_image_elim_on
modified theorem set.mem_image_eq
modified theorem set.mem_image_of_mem
added theorem set.mem_preimage_eq
deleted theorem set.mem_vimage_eq
modified theorem set.mono_image
added def set.preimage
added theorem set.preimage_comp
added theorem set.preimage_compl
added theorem set.preimage_empty
added theorem set.preimage_id
added theorem set.preimage_image_eq
added theorem set.preimage_inter
added theorem set.preimage_mono
added theorem set.preimage_union
added theorem set.preimage_univ
deleted def set.vimage
deleted theorem set.vimage_comp
deleted theorem set.vimage_compl
deleted theorem set.vimage_empty
deleted theorem set.vimage_id
deleted theorem set.vimage_image_eq
deleted theorem set.vimage_inter
deleted theorem set.vimage_mono
deleted theorem set.vimage_union
deleted theorem set.vimage_univ
added theorem set.monotone_preimage
deleted theorem set.monotone_vimage
added theorem set.preimage_Union
added theorem set.preimage_sUnion
deleted theorem set.vimage_Union
deleted theorem set.vimage_sUnion
modified def continuous
modified theorem open_induced