Revision #3297 → #3861 · back to history
modifiedLebesgue measure on Euclidean space70ed1c429cc2
| Field | From #3297 | To #3861 |
|---|
| mathlib.module | Mathlib.MeasureTheory.Measure.Lebesgue.Basic | Mathlib.MeasureTheory.Measure.Haar.OfBasis |
| note | Mathlib formalizes Lebesgue measure on `ℝ` via the `Real.measureSpace` instance providing `volume : Measure ℝ`, and lifts to `ℝⁿ` via the product Lebesgue measure. | Mathlib formalizes Lebesgue measure on `ℝ` via the `Real.measureSpace` instance (declared in `Mathlib.MeasureTheory.Measure.Haar.OfBasis`) providing `volume : Measure ℝ`, and lifts to `ℝⁿ` via the product Lebesgue measure. |
modifiedHyperreal numbersaaece3e02253
| Field | From #3297 | To #3861 |
|---|
| mathlib.module | Mathlib.Analysis.SpecificLimits.Hyperreal | Mathlib.Analysis.Real.Hyperreal |
| note | Mathlib defines `Hyperreal` as the ultraproduct `Germ (hyperfilter ℕ) ℝ`, providing the setting for non-standard analysis. | Mathlib defines `Hyperreal` (in `Mathlib.Analysis.Real.Hyperreal`) as the ultraproduct `Germ (hyperfilter ℕ) ℝ`, providing the setting for non-standard analysis. |
addedDifferential geometry6a955b65e264
addedDifferential topologyd031ac528867
addedCountable additivity of a measure8439209592e9