Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-28 18:07 4297eebb

View on Github →

feat(topology): add Borel spaces

Estimated changes

Modified data/set/basic.lean

deleted theorem set.image_preimage_subset

deleted theorem set.image_subset_eq

deleted theorem set.image_union_supset

deleted theorem set.inter_preimage_subset

deleted theorem set.preimage_diff

deleted theorem set.subset_preimage_image

deleted theorem set.union_preimage_subset

Modified data/set/countable.lean

modified theorem set.countable_empty

added theorem set.countable_set_of_finite_subset

modified theorem set.countable_singleton

Deleted data/set/function.lean

deleted theorem set.bij_on.mk

deleted def set.bij_on

deleted theorem set.bij_on_comp

deleted theorem set.bij_on_of_eq_on

deleted theorem set.bij_on_of_inv_on

deleted theorem set.bijective_iff_bij_on_univ

deleted theorem set.eq_on_of_left_inv_of_right_inv

deleted theorem set.image_eq_of_bij_on

deleted theorem set.image_eq_of_maps_to_of_surj_on

deleted theorem set.image_subset_of_maps_to

deleted theorem set.image_subset_of_maps_to_of_subset

deleted def set.inj_on

deleted theorem set.inj_on_comp

deleted theorem set.inj_on_empty

deleted theorem set.inj_on_of_bij_on

deleted theorem set.inj_on_of_eq_on

deleted theorem set.inj_on_of_inj_on_of_subset

deleted theorem set.inj_on_of_left_inv_on

deleted theorem set.injective_iff_inj_on_univ

deleted def set.inv_on

deleted def set.left_inv_on

deleted theorem set.left_inv_on_comp

deleted theorem set.left_inv_on_of_eq_on_left

deleted theorem set.left_inv_on_of_eq_on_right

deleted theorem set.left_inv_on_of_surj_on_right_inv_on

deleted def set.maps_to

deleted theorem set.maps_to_comp

deleted theorem set.maps_to_of_bij_on

deleted theorem set.maps_to_of_eq_on

deleted theorem set.maps_to_univ_univ

deleted def set.right_inv_on

deleted theorem set.right_inv_on_comp

deleted theorem set.right_inv_on_of_eq_on_left

deleted theorem set.right_inv_on_of_eq_on_right

deleted theorem set.right_inv_on_of_inj_on_of_left_inv_on

deleted def set.surj_on

deleted theorem set.surj_on_comp

deleted theorem set.surj_on_of_bij_on

deleted theorem set.surj_on_of_eq_on

deleted theorem set.surj_on_of_right_inv_on

deleted theorem set.surjective_iff_surj_on_univ

Modified data/set/lattice.lean

added theorem bind_def

added def disjoint

added theorem disjoint_bot_left

added theorem disjoint_bot_right

added theorem disjoint_symm

added theorem fmap_eq_image

added theorem image_Union

added theorem mem_seq_iff

added theorem monotone_preimage

added theorem preimage_Union

added theorem preimage_sUnion

added theorem set.Inter_neg

added theorem set.Inter_pos

added theorem set.Inter_univ

added theorem set.Union_empty

added theorem set.Union_neg

added theorem set.Union_pos

deleted theorem set.bind_def

deleted def set.disjoint

deleted theorem set.disjoint_bot_left

deleted theorem set.disjoint_bot_right

deleted theorem set.disjoint_symm

deleted theorem set.fmap_eq_image

deleted theorem set.image_Union

deleted theorem set.mem_seq_iff

deleted theorem set.monotone_preimage

deleted theorem set.preimage_Union

deleted theorem set.preimage_sUnion

added theorem set.sdiff_empty

added theorem set.sdiff_eq:

added theorem set.union_sdiff_left

added theorem set.union_sdiff_right

deleted theorem set.univ_subtype

added theorem univ_subtype

Modified order/complete_lattice.lean

added theorem lattice.infi_neg

added theorem lattice.infi_pos

added theorem lattice.supr_neg

added theorem lattice.supr_pos

Created topology/borel_space.lean

added theorem measure_theory.borel_comap

added theorem measure_theory.borel_eq_generate_from_of_subbasis

added theorem measure_theory.borel_prod

added theorem measure_theory.is_measurable_closure

added theorem measure_theory.is_measurable_interior

added theorem measure_theory.is_measurable_of_is_closed

added theorem measure_theory.is_measurable_of_is_open

added theorem measure_theory.measurable_add

added theorem measure_theory.measurable_mul

added theorem measure_theory.measurable_neg

added theorem measure_theory.measurable_of_continuous2

added theorem measure_theory.measurable_of_continuous

added theorem measure_theory.measurable_sub

Modified topology/measurable_space.lean

Modified topology/outer_measure.lean

deleted theorem Inter_neg

deleted theorem Inter_pos

deleted theorem Inter_univ

deleted theorem Union_empty

deleted theorem Union_neg

deleted theorem Union_pos

deleted theorem sdiff_empty

deleted theorem sdiff_eq:

deleted theorem union_sdiff_left

deleted theorem union_sdiff_right

Modified topology/topological_space.lean

added theorem is_open_sInter

added theorem topological_space.is_open_generated_countable_inter

Modified topology/topological_structures.lean

deleted theorem infi_neg

deleted theorem infi_pos

deleted theorem supr_neg

deleted theorem supr_pos