Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-28 18:08 c3aeb53b

View on Github →

feat(topology): add Lebesgue measure

Estimated changes

Modified algebra/field.lean

added theorem inv_lt_one

Modified data/rat.lean

Modified data/set/basic.lean

added theorem set.range_eq_image

Modified data/set/countable.lean

modified theorem set.countable_Union

added theorem set.countable_Union_Prop

added theorem set.countable_bUnion

Modified data/set/default.lean

Created data/set/intervals.lean

added def set.Ico

added theorem set.Ico_eq_Ico_iff

added theorem set.Ico_eq_empty

added theorem set.Ico_eq_empty_iff

added theorem set.Ico_inter_Iio_eq

added theorem set.Ico_sdiff_Iio_eq

added theorem set.Ico_subset_Ico_iff

added def set.Iio

added def set.Ioo

added theorem set.Ioo_eq_empty_of_ge

added theorem set.Ioo_inter_Ioo

Modified data/set/lattice.lean

added theorem set.sdiff_inter_same

added theorem set.sdiff_union_same

added theorem set.subset.antisymm_iff

added theorem set.union_of_subset_right

Modified logic/basic.lean

added theorem classical.or_not

Modified order/bounds.lean

added theorem ne_empty_of_is_glb

added theorem ne_empty_of_is_lub

Modified order/complete_lattice.lean

added theorem lattice.Inf_lt_iff

added theorem lattice.Sup_eq_top

added theorem lattice.infi_lt_iff

added theorem lattice.lt_Sup_iff

added theorem lattice.lt_supr_iff

Modified topology/borel_space.lean

added theorem measure_theory.is_measurable_Ico

added theorem measure_theory.is_measurable_Iio

added theorem measure_theory.is_measurable_Ioo

Modified topology/continuity.lean

added theorem prod_generate_from_generate_from_eq

Modified topology/ennreal.lean

deleted theorem Inf_lt_iff

deleted theorem Sup_eq_top

added theorem ennreal.add_infi

added theorem ennreal.add_sub_self

added theorem ennreal.infi_add

added theorem ennreal.infi_add_infi

added theorem ennreal.infi_of_real

added theorem ennreal.infi_sum

added theorem ennreal.infty_sub_of_real

deleted theorem ennreal.le_sub_iff_add_le

added theorem ennreal.of_real_le_of_real

added theorem ennreal.of_real_sub_of_real

added theorem ennreal.sub_supr

added theorem ennreal.supr_of_real

deleted theorem infi_lt_iff

deleted theorem lt_Sup_iff

deleted theorem lt_supr_iff

added theorem supr_bool_eq

Modified topology/lebesgue_measure.lean

deleted def Ico

deleted theorem Ico_eq_Ico_iff

deleted theorem Ico_eq_empty

deleted theorem Ico_eq_empty_iff

deleted theorem Ico_inter_Iio_eq

deleted theorem Ico_sdiff_Iio_eq

deleted theorem Ico_subset_Ico_iff

deleted def Iio

added theorem borel_eq_generate_from_Iio_of_rat

added theorem borel_eq_generate_from_Ioo_of_rat_of_rat

added theorem inv_le_inv

deleted theorem is_lub_of_is_lub_of_tendsto

added theorem is_topological_basis_Ioo_of_rat_of_rat

added theorem is_topological_basis_of_open_of_nhds

added theorem max_of_rat_of_rat

added def measure_theory.lebesgue

added theorem measure_theory.lebesgue_Ico

added theorem measure_theory.lebesgue_Ioo

added theorem measure_theory.lebesgue_singleton

added theorem measure_theory.tendsto_of_nat_at_top_at_top

added theorem min_of_rat_of_rat

deleted theorem nhds_principal_ne_top_of_is_lub

deleted theorem set.subset.antisymm_iff

Modified topology/limits.lean

added theorem of_nat_pos

Modified topology/measurable_space.lean

added theorem is_measurable_set_prod

added theorem measurable_fst

added theorem measurable_prod

added theorem measurable_prod_mk

added theorem measurable_snd

added theorem measurable_space.comap_generate_from

added theorem measurable_space.generate_from_le_generate_from

added theorem measurable_space.generate_from_sup_generate_from

added theorem measurable_subtype_mk

added theorem measurable_subtype_val

added theorem set.disjointed_of_mono

Modified topology/measure.lean

added theorem measure_theory.measure_Inter_eq_infi_nat

added theorem measure_theory.measure_Union_eq_supr_nat

deleted theorem measure_theory.measure_Union_le_nat

added theorem measure_theory.measure_Union_le_tsum_nat

modified theorem measure_theory.measure_empty

deleted theorem measure_theory.measure_eq_measure_of

modified theorem measure_theory.measure_mono

added theorem measure_theory.measure_sdiff

deleted def measure_theory.measure_space.measure

modified theorem measure_theory.measure_union

added def measure_theory.outer_measure.to_measure

deleted theorem supr_bool_eq

Modified topology/outer_measure.lean

deleted theorem classical.or_not

deleted theorem ennreal.add_infi

deleted theorem ennreal.infi_add

deleted theorem ennreal.infi_add_infi

deleted theorem ennreal.infi_sum

deleted theorem inv_lt_one

added theorem measure_theory.outer_measure.caratheodory_is_measurable

added theorem measure_theory.outer_measure.caratheodory_is_measurable_eq

deleted def measure_theory.outer_measure.inf

deleted theorem measure_theory.outer_measure.inf_space_is_measurable

deleted def measure_theory.outer_measure.measure

deleted def measure_theory.outer_measure.space

deleted theorem measure_theory.outer_measure.space_is_measurable_eq

Modified topology/real.lean

added theorem exists_gt_of_rat

added theorem exists_lt_of_rat_of_rat_gt

Modified topology/topological_space.lean

added theorem induced_le_iff_le_coinduced

added def topological_space.is_topological_basis

added theorem topological_space.is_topological_basis_of_subbasis

added theorem topological_space.mem_nhds_of_is_topological_basis

Modified topology/topological_structures.lean

added theorem closure_compl

added theorem closure_le_eq

added theorem continuous_if

added theorem continuous_max

added theorem continuous_min

added theorem continuous_sub'

added def frontier

added theorem frontier_eq_closure_inter_closure

added theorem frontier_le_subset_eq

added theorem interior_compl

added theorem is_glb_of_is_glb_of_tendsto

added theorem is_glb_of_is_lub_of_tendsto

added theorem is_glb_of_mem_nhds

added theorem is_lub_of_is_lub_of_tendsto

added theorem is_lub_of_mem_nhds

added theorem is_open_Iio

added theorem is_open_Ioo

added theorem nhds_principal_ne_bot_of_is_glb

added theorem nhds_principal_ne_bot_of_is_lub

added theorem tendsto_max

added theorem tendsto_min