Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-07 20:30 1b36dabc

View on Github →

refactor(data/set/basic): move image, preimage, and range to a new file (#17842) This means data.set.basic is mainly about lattice operations. Only one proof is modified (to avoid it needing to move between files). All other lemmas are copied verbatim.

Estimated changes

deleted theorem nat.mem_range_succ
deleted theorem option.injective_iff
deleted theorem option.range_eq
deleted theorem prod.range_fst
deleted theorem prod.range_snd
deleted theorem set.apply_range_splitting
deleted theorem set.ball_image_iff
deleted theorem set.ball_image_of_ball
deleted theorem set.bex_image_iff
deleted theorem set.comp_range_splitting
deleted theorem set.compl_compl_image
deleted theorem set.compl_image
deleted theorem set.compl_image_set_of
deleted theorem set.compl_range_inl
deleted theorem set.compl_range_inr
deleted theorem set.compl_range_some
deleted theorem set.exists_image_iff
deleted theorem set.exists_range_iff'
deleted theorem set.exists_range_iff
deleted theorem set.forall_range_iff
deleted def set.image
deleted theorem set.image_comm
deleted theorem set.image_comp
deleted theorem set.image_compl_eq
deleted theorem set.image_compl_preimage
deleted theorem set.image_compl_subset
deleted theorem set.image_congr'
deleted theorem set.image_congr
deleted theorem set.image_diff
deleted theorem set.image_diff_preimage
deleted theorem set.image_empty
deleted theorem set.image_eq_empty
deleted theorem set.image_eq_image
deleted theorem set.image_eq_range
deleted theorem set.image_eta
deleted theorem set.image_id'
deleted theorem set.image_id
deleted theorem set.image_image
deleted theorem set.image_injective
deleted theorem set.image_insert_eq
deleted theorem set.image_inter
deleted theorem set.image_inter_on
deleted theorem set.image_inter_preimage
deleted theorem set.image_inter_subset
deleted theorem set.image_pair
deleted theorem set.image_perm
deleted theorem set.image_preimage_eq
deleted theorem set.image_preimage_eq_iff
deleted theorem set.image_preimage_inter
deleted theorem set.image_preimage_subset
deleted theorem set.image_singleton
deleted theorem set.image_subset
deleted theorem set.image_subset_iff
deleted theorem set.image_subset_range
deleted theorem set.image_surjective
deleted theorem set.image_symm_diff
deleted theorem set.image_union
deleted theorem set.image_univ
deleted theorem set.inter_preimage_subset
deleted theorem set.mem_compl_image
deleted theorem set.mem_image
deleted theorem set.mem_image_elim
deleted theorem set.mem_image_elim_on
deleted theorem set.mem_image_iff_bex
deleted theorem set.mem_image_of_mem
deleted theorem set.mem_preimage
deleted theorem set.mem_range
deleted theorem set.mem_range_self
deleted theorem set.nonempty.image
deleted theorem set.nonempty.image_const
deleted theorem set.nonempty.of_image
deleted theorem set.nonempty.preimage'
deleted theorem set.nonempty.preimage
deleted theorem set.nonempty_image_iff
deleted theorem set.nontrivial.image
deleted theorem set.nontrivial.preimage
deleted theorem set.nontrivial_of_image
deleted def set.preimage
deleted theorem set.preimage_comp
deleted theorem set.preimage_comp_eq
deleted theorem set.preimage_compl
deleted theorem set.preimage_congr
deleted theorem set.preimage_const
deleted theorem set.preimage_const_of_mem
deleted theorem set.preimage_diff
deleted theorem set.preimage_empty
deleted theorem set.preimage_eq_preimage'
deleted theorem set.preimage_eq_preimage
deleted theorem set.preimage_id'
deleted theorem set.preimage_id
deleted theorem set.preimage_id_eq
deleted theorem set.preimage_image_eq
deleted theorem set.preimage_injective
deleted theorem set.preimage_inter
deleted theorem set.preimage_inter_range
deleted theorem set.preimage_ite
deleted theorem set.preimage_iterate_eq
deleted theorem set.preimage_mono
deleted theorem set.preimage_preimage
deleted theorem set.preimage_range
deleted theorem set.preimage_range_inter
deleted theorem set.preimage_set_of_eq
deleted theorem set.preimage_subset_iff
deleted theorem set.preimage_surjective
deleted theorem set.preimage_union
deleted theorem set.preimage_univ
deleted def set.range
deleted theorem set.range_comp
deleted theorem set.range_const
deleted theorem set.range_const_subset
deleted theorem set.range_diff_image
deleted theorem set.range_eq_empty
deleted theorem set.range_eq_empty_iff
deleted theorem set.range_eq_iff
deleted theorem set.range_eval
deleted theorem set.range_id'
deleted theorem set.range_id
deleted theorem set.range_iff_surjective
deleted theorem set.range_image
deleted theorem set.range_inclusion
deleted theorem set.range_ite_subset'
deleted theorem set.range_ite_subset
deleted theorem set.range_nonempty
deleted theorem set.range_quot_lift
deleted theorem set.range_quot_mk
deleted theorem set.range_quotient_lift
deleted theorem set.range_quotient_mk'
deleted theorem set.range_quotient_mk
deleted theorem set.range_some_inter_none
deleted theorem set.range_some_union_none
deleted theorem set.range_subset_iff
deleted theorem set.range_subtype_map
deleted theorem set.range_unique
deleted theorem set.subset_image_compl
deleted theorem set.subset_image_diff
deleted theorem set.subset_image_union
deleted theorem set.subset_preimage_image
deleted theorem set.subset_preimage_univ
deleted theorem set.subsingleton.image
deleted theorem set.subsingleton.preimage
deleted theorem set.subsingleton_of_image
deleted theorem set.subsingleton_range
deleted theorem set.sum.elim_range
deleted theorem set.surjective_onto_image
deleted theorem set.surjective_onto_range
deleted theorem set.union_preimage_subset
deleted theorem subtype.coe_image
deleted theorem subtype.coe_image_subset
deleted theorem subtype.coe_image_univ
deleted theorem subtype.coe_preimage_self
deleted theorem subtype.range_coe
deleted theorem subtype.range_coe_subtype
deleted theorem subtype.range_val
deleted theorem subtype.range_val_subtype
deleted theorem sum.range_eq
deleted theorem with_bot.range_eq
deleted theorem with_top.range_eq
added theorem nat.mem_range_succ
added theorem option.injective_iff
added theorem option.range_eq
added theorem prod.range_fst
added theorem prod.range_snd
added theorem set.ball_image_iff
added theorem set.ball_image_of_ball
added theorem set.bex_image_iff
added theorem set.compl_compl_image
added theorem set.compl_image
added theorem set.compl_image_set_of
added theorem set.compl_range_inl
added theorem set.compl_range_inr
added theorem set.compl_range_some
added theorem set.exists_image_iff
added theorem set.exists_range_iff'
added theorem set.exists_range_iff
added theorem set.forall_range_iff
added def set.image
added theorem set.image_comm
added theorem set.image_comp
added theorem set.image_compl_eq
added theorem set.image_compl_subset
added theorem set.image_congr'
added theorem set.image_congr
added theorem set.image_diff
added theorem set.image_empty
added theorem set.image_eq_empty
added theorem set.image_eq_image
added theorem set.image_eq_range
added theorem set.image_eta
added theorem set.image_id'
added theorem set.image_id
added theorem set.image_image
added theorem set.image_injective
added theorem set.image_insert_eq
added theorem set.image_inter
added theorem set.image_inter_on
added theorem set.image_inter_subset
added theorem set.image_pair
added theorem set.image_perm
added theorem set.image_preimage_eq
added theorem set.image_singleton
added theorem set.image_subset
added theorem set.image_subset_iff
added theorem set.image_subset_range
added theorem set.image_surjective
added theorem set.image_symm_diff
added theorem set.image_union
added theorem set.image_univ
added theorem set.mem_compl_image
added theorem set.mem_image
added theorem set.mem_image_elim
added theorem set.mem_image_elim_on
added theorem set.mem_image_iff_bex
added theorem set.mem_image_of_mem
added theorem set.mem_preimage
added theorem set.mem_range
added theorem set.mem_range_self
added theorem set.nonempty.image
added theorem set.nonempty.of_image
added theorem set.nonempty.preimage'
added theorem set.nonempty.preimage
added theorem set.nonempty_image_iff
added theorem set.nontrivial.image
added def set.preimage
added theorem set.preimage_comp
added theorem set.preimage_comp_eq
added theorem set.preimage_compl
added theorem set.preimage_congr
added theorem set.preimage_const
added theorem set.preimage_diff
added theorem set.preimage_empty
added theorem set.preimage_id'
added theorem set.preimage_id
added theorem set.preimage_id_eq
added theorem set.preimage_image_eq
added theorem set.preimage_injective
added theorem set.preimage_inter
added theorem set.preimage_ite
added theorem set.preimage_mono
added theorem set.preimage_preimage
added theorem set.preimage_range
added theorem set.preimage_set_of_eq
added theorem set.preimage_union
added theorem set.preimage_univ
added def set.range
added theorem set.range_comp
added theorem set.range_const
added theorem set.range_const_subset
added theorem set.range_diff_image
added theorem set.range_eq_empty
added theorem set.range_eq_empty_iff
added theorem set.range_eq_iff
added theorem set.range_eval
added theorem set.range_id'
added theorem set.range_id
added theorem set.range_image
added theorem set.range_inclusion
added theorem set.range_ite_subset'
added theorem set.range_ite_subset
added theorem set.range_nonempty
added theorem set.range_quot_lift
added theorem set.range_quot_mk
added theorem set.range_quotient_mk'
added theorem set.range_quotient_mk
added theorem set.range_subset_iff
added theorem set.range_subtype_map
added theorem set.range_unique
added theorem set.subset_image_compl
added theorem set.subset_image_diff
added theorem set.subset_image_union
added theorem set.subsingleton.image
added theorem set.subsingleton_range
added theorem set.sum.elim_range
added theorem subtype.coe_image
added theorem subtype.coe_image_univ
added theorem subtype.range_coe
added theorem subtype.range_val
added theorem sum.range_eq
added theorem with_bot.range_eq
added theorem with_top.range_eq