Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-22 12:52 865ba360

View on Github →

feat(data/set): add functions over sets

Estimated changes

Modified data/set/basic.lean

added theorem set.image_preimage_subset

added theorem set.image_subset_eq

added theorem set.image_union_supset

added theorem set.inter_preimage_subset

added theorem set.preimage_diff

added theorem set.subset_preimage_image

added theorem set.union_preimage_subset

Modified data/set/countable.lean

modified theorem set.countable_empty

deleted theorem set.countable_set_of_finite_subset

modified theorem set.countable_singleton

Created data/set/function.lean

added theorem set.bij_on.mk

added def set.bij_on

added theorem set.bij_on_comp

added theorem set.bij_on_of_eq_on

added theorem set.bij_on_of_inv_on

added theorem set.bijective_iff_bij_on_univ

added theorem set.eq_on_of_left_inv_of_right_inv

added theorem set.image_eq_of_bij_on

added theorem set.image_eq_of_maps_to_of_surj_on

added theorem set.image_subset_of_maps_to

added theorem set.image_subset_of_maps_to_of_subset

added def set.inj_on

added theorem set.inj_on_comp

added theorem set.inj_on_empty

added theorem set.inj_on_of_bij_on

added theorem set.inj_on_of_eq_on

added theorem set.inj_on_of_inj_on_of_subset

added theorem set.inj_on_of_left_inv_on

added theorem set.injective_iff_inj_on_univ

added def set.inv_on

added def set.left_inv_on

added theorem set.left_inv_on_comp

added theorem set.left_inv_on_of_eq_on_left

added theorem set.left_inv_on_of_eq_on_right

added theorem set.left_inv_on_of_surj_on_right_inv_on

added def set.maps_to

added theorem set.maps_to_comp

added theorem set.maps_to_of_bij_on

added theorem set.maps_to_of_eq_on

added theorem set.maps_to_univ_univ

added def set.right_inv_on

added theorem set.right_inv_on_comp

added theorem set.right_inv_on_of_eq_on_left

added theorem set.right_inv_on_of_eq_on_right

added theorem set.right_inv_on_of_inj_on_of_left_inv_on

added def set.surj_on

added theorem set.surj_on_comp

added theorem set.surj_on_of_bij_on

added theorem set.surj_on_of_eq_on

added theorem set.surj_on_of_right_inv_on

added theorem set.surjective_iff_surj_on_univ

Modified data/set/lattice.lean

deleted theorem bind_def

deleted def disjoint

deleted theorem disjoint_bot_left

deleted theorem disjoint_bot_right

deleted theorem disjoint_symm

deleted theorem fmap_eq_image

deleted theorem image_Union

deleted theorem mem_seq_iff

deleted theorem monotone_preimage

deleted theorem preimage_Union

deleted theorem preimage_sUnion

deleted theorem set.Inter_neg

deleted theorem set.Inter_pos

deleted theorem set.Inter_univ

deleted theorem set.Union_empty

deleted theorem set.Union_neg

deleted theorem set.Union_pos

added theorem set.bind_def

added def set.disjoint

added theorem set.disjoint_bot_left

added theorem set.disjoint_bot_right

added theorem set.disjoint_symm

added theorem set.fmap_eq_image

added theorem set.image_Union

added theorem set.mem_seq_iff

added theorem set.monotone_preimage

added theorem set.preimage_Union

added theorem set.preimage_sUnion

deleted theorem set.sdiff_empty

deleted theorem set.sdiff_eq:

deleted theorem set.union_sdiff_left

deleted theorem set.union_sdiff_right

added theorem set.univ_subtype

deleted theorem univ_subtype

Modified order/complete_lattice.lean

deleted theorem lattice.infi_neg

deleted theorem lattice.infi_pos

deleted theorem lattice.supr_neg

deleted theorem lattice.supr_pos

Modified topology/measurable_space.lean

Modified topology/outer_measure.lean

added theorem Inter_neg

added theorem Inter_pos

added theorem Inter_univ

added theorem Union_empty

added theorem Union_neg

added theorem Union_pos

added theorem sdiff_empty

added theorem sdiff_eq:

added theorem union_sdiff_left

added theorem union_sdiff_right

Modified topology/topological_space.lean

deleted theorem is_open_sInter

deleted theorem topological_space.is_open_generated_countable_inter

Modified topology/topological_structures.lean

added theorem infi_neg

added theorem infi_pos

added theorem supr_neg

added theorem supr_pos