Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-19 15:34 29639b31

View on Github →

feat(analysis/measure_theory): optimize proofs; trim, is_complete

Estimated changes

Modified algebra/ordered_field.lean

added theorem one_half_lt_one

added theorem one_half_pos

Modified analysis/ennreal.lean

added theorem ennreal.add_left_inj

added theorem ennreal.add_right_inj

added theorem ennreal.add_sub_self'

added theorem ennreal.add_supr

added theorem ennreal.exists_pos_sum_of_encodable

added theorem ennreal.of_real_add_le

added theorem ennreal.sub_infi

added theorem ennreal.sub_le_self

added theorem ennreal.sub_sub_cancel

modified theorem ennreal.sub_supr

added theorem ennreal.supr_add_supr

Modified analysis/limits.lean

added theorem is_sum_geometric_two

added def pos_sum_of_encodable

Modified analysis/measure_theory/borel_space.lean

added def measure_theory.borel

deleted theorem measure_theory.borel_eq_generate_from_Iio_rat

deleted theorem measure_theory.borel_eq_generate_from_Ioo_rat

added theorem measure_theory.borel_prod_le

deleted theorem measure_theory.is_topological_basis_Ioo_rat

added theorem real.borel_eq_generate_from_Iio_rat

added theorem real.borel_eq_generate_from_Ioo_rat

Modified analysis/measure_theory/lebesgue_measure.lean

added theorem measure_theory.is_lebesgue_measurable_Iio

deleted theorem measure_theory.le_lebesgue_length

modified def measure_theory.lebesgue

added theorem measure_theory.lebesgue_Icc

modified def measure_theory.lebesgue_length

added theorem measure_theory.lebesgue_length_Icc

deleted theorem measure_theory.lebesgue_length_Ico'

modified theorem measure_theory.lebesgue_length_Ico

added theorem measure_theory.lebesgue_length_Ioo

added theorem measure_theory.lebesgue_length_eq_infi_Icc

added theorem measure_theory.lebesgue_length_eq_infi_Ioo

added theorem measure_theory.lebesgue_length_mono

added theorem measure_theory.lebesgue_outer_Icc

modified theorem measure_theory.lebesgue_outer_Ico

added theorem measure_theory.lebesgue_outer_Ioo

deleted theorem measure_theory.lebesgue_outer_is_measurable_Iio

added theorem measure_theory.lebesgue_outer_le_length

added theorem measure_theory.lebesgue_outer_singleton

added theorem measure_theory.lebesgue_outer_trim

modified theorem measure_theory.lebesgue_singleton

added theorem measure_theory.lebesgue_to_outer_measure

added theorem measure_theory.lebesgue_val

deleted theorem measure_theory.tendsto_of_nat_at_top_at_top

Modified analysis/measure_theory/measurable_space.lean

added theorem encodable.Union_decode2

added theorem encodable.Union_decode2_cases

added theorem is_measurable.Inter

added theorem is_measurable.Union

added theorem is_measurable.bInter

added theorem is_measurable.bUnion

added theorem is_measurable.compl

added theorem is_measurable.compl_iff

added theorem is_measurable.diff

added theorem is_measurable.disjointed

added theorem is_measurable.empty

added theorem is_measurable.inter

added theorem is_measurable.sInter

added theorem is_measurable.sUnion

added theorem is_measurable.sub

added theorem is_measurable.union

modified def is_measurable

deleted theorem is_measurable_Inter

deleted theorem is_measurable_Union

deleted theorem is_measurable_Union_nat

deleted theorem is_measurable_bInter

deleted theorem is_measurable_bUnion

deleted theorem is_measurable_compl

deleted theorem is_measurable_disjointed

deleted theorem is_measurable_empty

deleted theorem is_measurable_inter

deleted theorem is_measurable_sInter

deleted theorem is_measurable_sUnion

deleted theorem is_measurable_sdiff

deleted theorem is_measurable_sub

deleted theorem is_measurable_union

added theorem measurable.comp

added theorem measurable.if

added theorem measurable.preimage

added theorem measurable.prod

deleted theorem measurable_comp

deleted theorem measurable_if

deleted theorem measurable_prod

added theorem measurable_space.Union_decode2_disjoint_on

deleted theorem measurable_space.dynkin_system.dynkin_system_eq

added theorem measurable_space.dynkin_system.ext

modified theorem measurable_space.dynkin_system.generate_le

added theorem measurable_space.dynkin_system.has_Union

added theorem measurable_space.dynkin_system.has_compl_iff

added theorem measurable_space.dynkin_system.has_diff

deleted theorem measurable_space.dynkin_system.has_sdiff

modified theorem measurable_space.dynkin_system.has_union

modified def measurable_space.dynkin_system.restrict_on

added theorem measurable_space.ext

added theorem measurable_space.is_measurable_Inf

added theorem measurable_space.is_measurable_inf

added theorem measurable_space.is_measurable_infi

deleted theorem measurable_space_eq

Modified analysis/measure_theory/measure_space.lean

added def completion

added theorem is_measurable.diff_null

added theorem is_measurable.is_null_measurable

added theorem is_null_measurable.Union_nat

added theorem is_null_measurable.compl

added theorem is_null_measurable.diff_null

added theorem is_null_measurable.union_null

added def is_null_measurable

added theorem is_null_measurable_iff

added theorem is_null_measurable_measure_eq

added theorem is_null_measurable_of_complete

modified theorem measure_theory.le_to_outer_measure_caratheodory

added def measure_theory.measure'

added theorem measure_theory.measure'_Union

added theorem measure_theory.measure'_Union_le_tsum_nat'

added theorem measure_theory.measure'_Union_le_tsum_nat

added theorem measure_theory.measure'_Union_nat

added theorem measure_theory.measure'_empty

added theorem measure_theory.measure'_eq

added theorem measure_theory.measure'_mono

added theorem measure_theory.measure'_union

added theorem measure_theory.measure.add_apply

added theorem measure_theory.measure.add_to_outer_measure

added def measure_theory.measure.count

added def measure_theory.measure.dirac

added theorem measure_theory.measure.dirac_apply

added theorem measure_theory.measure.ext

added def measure_theory.measure.is_complete

added theorem measure_theory.measure.le_iff'

added theorem measure_theory.measure.le_iff

added def measure_theory.measure.map

added theorem measure_theory.measure.map_apply

added theorem measure_theory.measure.map_id

added theorem measure_theory.measure.map_map

added def measure_theory.measure.of_measurable

added def measure_theory.measure.sum

added theorem measure_theory.measure.to_outer_measure_le

added theorem measure_theory.measure.zero_apply

added theorem measure_theory.measure.zero_to_outer_measure

added structure measure_theory.measure

added theorem measure_theory.measure_Union

added theorem measure_theory.measure_Union_le

deleted theorem measure_theory.measure_Union_le_tsum_nat

deleted theorem measure_theory.measure_Union_nat

added theorem measure_theory.measure_Union_null

modified theorem measure_theory.measure_bUnion

added theorem measure_theory.measure_diff

modified theorem measure_theory.measure_empty

added theorem measure_theory.measure_eq_infi

added theorem measure_theory.measure_eq_measure'

added theorem measure_theory.measure_eq_outer_measure'

added theorem measure_theory.measure_eq_trim

modified theorem measure_theory.measure_mono

added theorem measure_theory.measure_mono_null

modified theorem measure_theory.measure_sUnion

deleted theorem measure_theory.measure_sdiff

deleted def measure_theory.measure_space.count

deleted def measure_theory.measure_space.dirac

deleted def measure_theory.measure_space.map

deleted theorem measure_theory.measure_space.map_comp

deleted theorem measure_theory.measure_space.map_id

deleted theorem measure_theory.measure_space.map_measure

deleted def measure_theory.measure_space.sum

deleted structure measure_theory.measure_space

deleted theorem measure_theory.measure_space_eq

deleted theorem measure_theory.measure_space_eq_of

added theorem measure_theory.measure_union_le

added theorem measure_theory.measure_union_null

added def measure_theory.outer_measure'

added theorem measure_theory.outer_measure'_eq

added theorem measure_theory.outer_measure'_eq_measure'

added theorem measure_theory.outer_measure.le_trim_iff

modified def measure_theory.outer_measure.to_measure

added def measure_theory.outer_measure.trim

added theorem measure_theory.outer_measure.trim_add

added theorem measure_theory.outer_measure.trim_congr

added theorem measure_theory.outer_measure.trim_eq

added theorem measure_theory.outer_measure.trim_eq_infi'

added theorem measure_theory.outer_measure.trim_eq_infi

added theorem measure_theory.outer_measure.trim_ge

added theorem measure_theory.outer_measure.trim_le_trim

added theorem measure_theory.outer_measure.trim_sum_ge

added theorem measure_theory.outer_measure.trim_trim

added theorem measure_theory.outer_measure.trim_zero

added theorem measure_theory.to_measure_apply

added theorem measure_theory.to_measure_to_outer_measure

added theorem measure_theory.to_outer_measure_apply

added theorem measure_theory.to_outer_measure_eq_outer_measure'

modified theorem measure_theory.to_outer_measure_to_measure

added theorem null_is_null_measurable

added def null_measurable

Modified analysis/measure_theory/outer_measure.lean

added theorem measure_theory.outer_measure.Sup_apply

added theorem measure_theory.outer_measure.Union_aux

added theorem measure_theory.outer_measure.Union_null

added theorem measure_theory.outer_measure.add_apply

added theorem measure_theory.outer_measure.add_smul

deleted theorem measure_theory.outer_measure.caratheodory_is_measurable_eq

added def measure_theory.outer_measure.dirac

added theorem measure_theory.outer_measure.dirac_apply

added theorem measure_theory.outer_measure.dirac_caratheodory

added theorem measure_theory.outer_measure.empty'

added theorem measure_theory.outer_measure.ext

added theorem measure_theory.outer_measure.is_caratheodory

added theorem measure_theory.outer_measure.is_caratheodory_le

added theorem measure_theory.outer_measure.le_add_caratheodory

added theorem measure_theory.outer_measure.le_of_function

added theorem measure_theory.outer_measure.le_smul_caratheodory

added theorem measure_theory.outer_measure.le_sum_caratheodory

added def measure_theory.outer_measure.map

added theorem measure_theory.outer_measure.map_apply

added theorem measure_theory.outer_measure.map_id

added theorem measure_theory.outer_measure.map_map

added theorem measure_theory.outer_measure.mono'

added theorem measure_theory.outer_measure.mul_smul

added theorem measure_theory.outer_measure.one_smul

deleted theorem measure_theory.outer_measure.outer_measure_eq

added def measure_theory.outer_measure.smul

added theorem measure_theory.outer_measure.smul_add

added theorem measure_theory.outer_measure.smul_apply

added theorem measure_theory.outer_measure.smul_dirac_apply

added theorem measure_theory.outer_measure.smul_zero

deleted theorem measure_theory.outer_measure.subadditive

added def measure_theory.outer_measure.sum

added theorem measure_theory.outer_measure.sum_apply

added theorem measure_theory.outer_measure.sup_apply

added theorem measure_theory.outer_measure.supr_apply

added theorem measure_theory.outer_measure.top_apply

added theorem measure_theory.outer_measure.union_null

added theorem measure_theory.outer_measure.zero_apply

added theorem measure_theory.outer_measure.zero_caratheodory

added theorem measure_theory.outer_measure.zero_smul

Modified analysis/real.lean

added theorem compact_Icc

deleted theorem compact_ivl

modified theorem rat.totally_bounded_Icc

added theorem real.is_topological_basis_Ioo_rat

modified theorem real.totally_bounded_Icc

added theorem tendsto_of_nat_at_top_at_top

Modified analysis/topology/infinite_sum.lean

modified theorem has_sum_mul_left

modified theorem has_sum_mul_right

modified theorem is_sum_mul_left

modified theorem is_sum_mul_right

added theorem tsum_equiv

added theorem tsum_fintype

modified theorem tsum_mul_left

modified theorem tsum_mul_right

Modified analysis/topology/topological_space.lean

added theorem topological_space.is_open_sUnion_countable

Modified analysis/topology/topological_structures.lean

modified theorem closure_le_eq

added theorem is_closed_Icc

Modified data/set/basic.lean

modified theorem set.mem_diff

deleted theorem set.mem_diff_eq

deleted theorem set.mem_diff_iff

added theorem set.mem_diff_of_mem

added theorem set.union_diff_distrib

Modified data/set/countable.lean

Modified data/set/disjointed.lean

added theorem pairwise_disjoint_on_bool

added theorem pairwise_on_bool

added theorem set.Inter_lt_succ

added theorem set.Union_disjointed

added theorem set.Union_disjointed_of_mono

added theorem set.Union_lt_succ

deleted theorem set.disjointed_Union

Modified data/set/intervals.lean

added def set.Icc

added theorem set.Icc_diff_Ico_eq_singleton

added theorem set.Icc_eq_empty

added theorem set.Icc_eq_empty_iff

added theorem set.Icc_self

added theorem set.Icc_subset_Icc

added theorem set.Icc_subset_Icc_left

added theorem set.Icc_subset_Icc_right

added theorem set.Icc_subset_Ico_right

added theorem set.Ico_diff_Iio

added theorem set.Ico_diff_Ioo_eq_singleton

modified theorem set.Ico_eq_Ico_iff

modified theorem set.Ico_eq_empty

modified theorem set.Ico_eq_empty_iff

added theorem set.Ico_inter_Iio

deleted theorem set.Ico_inter_Iio_eq

deleted theorem set.Ico_sdiff_Iio_eq

deleted theorem set.Ico_sdiff_Ioo_eq_singleton

modified theorem set.Ico_self

added theorem set.Ico_subset_Icc_self

added theorem set.Ico_subset_Ico

modified theorem set.Ico_subset_Ico_iff

modified theorem set.Ico_subset_Ico_left

modified theorem set.Ico_subset_Ico_right

modified theorem set.Ico_subset_Iio_self

added theorem set.Iio_ne_empty

added theorem set.Ioo_eq_empty

added theorem set.Ioo_eq_empty_iff

deleted theorem set.Ioo_eq_empty_of_ge

modified theorem set.Ioo_self

added theorem set.Ioo_subset_Icc_self

modified theorem set.Ioo_subset_Ico_self

added theorem set.Ioo_subset_Ioo

added theorem set.Ioo_subset_Ioo_iff

added theorem set.Ioo_subset_Ioo_left

added theorem set.Ioo_subset_Ioo_right

added theorem set.mem_Icc

added theorem set.mem_Ico

added theorem set.mem_Iio

added theorem set.mem_Ioo

Modified order/complete_lattice.lean

modified theorem lattice.infi_and

modified theorem lattice.infi_prod

modified theorem lattice.infi_sigma

modified theorem lattice.infi_subtype

modified theorem lattice.supr_and

modified theorem lattice.supr_prod

modified theorem lattice.supr_sigma

modified theorem lattice.supr_subtype