Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-13 17:34 f705963c

View on Github →

feat(topology/measure): introduce measures

Estimated changes

Modified data/set/lattice.lean

modified theorem set.Union_subset_Union2

modified theorem set.inter_distrib_Union_left

added theorem set.inter_distrib_Union_right

Modified topology/ennreal.lean

deleted theorem ennreal.add_le_add

deleted theorem ennreal.lt_of_add_lt_add_left

added theorem lt_supr_iff

Modified topology/infinite_sum.lean

added theorem has_sum_sigma

added theorem is_sum_iff_is_sum_of_iso

added theorem is_sum_le

added theorem tsum_eq_sum

added theorem tsum_eq_tsum_of_is_sum_iff_is_sum

added theorem tsum_eq_tsum_of_iso

added theorem tsum_eq_tsum_of_ne_zero_bij

added theorem tsum_le_tsum

added theorem tsum_sigma

Modified topology/measurable_space.lean

added theorem is_measurable_disjointed

added def pairwise

modified theorem set.disjoint_disjointed

added theorem set.disjointed_induct

Created topology/measure.lean

added def measure_theory.count

added theorem measure_theory.measure_Union_le_nat

added theorem measure_theory.measure_Union_nat

added theorem measure_theory.measure_bUnion

added theorem measure_theory.measure_empty

added theorem measure_theory.measure_eq_measure_of

added theorem measure_theory.measure_mono

added theorem measure_theory.measure_sUnion

added def measure_theory.measure_space.measure

added structure measure_theory.measure_space

added theorem measure_theory.measure_space_eq

added theorem measure_theory.measure_space_eq_of

added theorem measure_theory.measure_union

added theorem supr_bool_eq

Modified topology/topological_structures.lean

modified theorem binfi_inf

added theorem inf_principal_eq_bot

added theorem infi_neg

added theorem infi_pos

modified theorem le_of_tendsto

deleted theorem mem_nhds_lattice_unbounded

added theorem mem_nhds_orderable_dest

added theorem mem_nhds_unbounded

added theorem supr_neg

added theorem supr_pos