Mathlib Changelog
Changelog
About
Github
Commit
2017-08-02 22:32
64b61515
View on Github →
refactor(data/set/basic,*): vimage -> preimage, add notation
Estimated changes
Modified
algebra/lattice/filter.lean
modified
theorem
filter.mem_vmap_of_mem
added
theorem
filter.preimage_mem_vmap
deleted
theorem
filter.vimage_mem_vmap
modified
theorem
filter.vmap_principal
added
theorem
set.image_eq_preimage_of_inverse
deleted
theorem
set.image_eq_vimage_of_inverse
added
theorem
set.image_swap_eq_preimage_swap
deleted
theorem
set.image_swap_eq_vimage_swap
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
data/set/basic.lean
added
theorem
set.eq_preimage_subtype_val_iff
deleted
theorem
set.eq_vimage_subtype_val_iff
modified
theorem
set.image_comp
modified
theorem
set.image_empty
modified
theorem
set.image_id
modified
theorem
set.image_subset
added
theorem
set.image_subset_iff_subset_preimage
deleted
theorem
set.image_subset_iff_subset_vimage
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
Modified
data/set/lattice.lean
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
topology/continuity.lean
modified
def
continuous
modified
theorem
open_induced
Modified
topology/topological_space.lean
Modified
topology/uniform_space.lean