Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-30 20:25 97036e7c

View on Github →

feat(measure_theory/constructions/pi): volume on α × α as a map of volume on fin 2 → α (#9432)

Estimated changes

Modified src/data/equiv/fin.lean

added def fin_two_arrow_equiv

added def order_iso.fin_two_arrow_iso

added def order_iso.pi_fin_two_iso

added def pi_fin_two_equiv

added def prod_equiv_pi_fin_two

Modified src/data/fin.lean

added theorem fin.exists_fin_one

added theorem fin.exists_fin_two

added theorem fin.forall_fin_one

added theorem fin.forall_fin_two

added theorem fin.insert_nth_apply_above

added theorem fin.insert_nth_apply_below

added theorem fin.zero_lt_one

Modified src/data/matrix/notation.lean

added theorem matrix.vec_cons_const

added theorem matrix.vec_single_eq_const

Modified src/measure_theory/constructions/pi.lean

added theorem measure_theory.integral_fin_two_arrow'

added theorem measure_theory.integral_fin_two_arrow

added theorem measure_theory.integral_fin_two_arrow_pi'

added theorem measure_theory.integral_fin_two_arrow_pi

added theorem measure_theory.measure.prod_eq_map_fin_two_arrow

added theorem measure_theory.measure.prod_eq_map_fin_two_arrow_same

added theorem measure_theory.measure.{u}

added theorem measure_theory.set_integral_fin_two_arrow'

added theorem measure_theory.set_integral_fin_two_arrow

added theorem measure_theory.set_integral_fin_two_arrow_pi'

added theorem measure_theory.set_integral_fin_two_arrow_pi

Modified src/measure_theory/measurable_space.lean

added def measurable_equiv.fin_two_arrow

added def measurable_equiv.pi_fin_two