Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
  2. HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
  3. HOL-Analysis: move gauges and (tagged) divisions to its own theory file
  4. HOL-Analysis: add cover lemma ported by L. C. Paulson
Changeset 63959:f77dca1abf1b by hoelzl:
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
The file was modified src/HOL/Analysis/Complete_Measure.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Set.thy (diff)
Changeset 63958:02de4a58e210 by hoelzl:
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
The file was modified src/HOL/Analysis/Complete_Measure.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Analysis/Set_Integral.thy (diff)
The file was modified src/HOL/Library/Indicator_Function.thy (diff)
Changeset 63957:c3da799b1b45 by hoelzl:
HOL-Analysis: move gauges and (tagged) divisions to its own theory file
The file was addedsrc/HOL/Analysis/Tagged_Division.thy
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
Changeset 63956:b235e845c8e8 by hoelzl:
HOL-Analysis: add cover lemma ported by L. C. Paulson
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)