Mathlib Changelog
v3
Changelog
About
Github
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