Revision #1386 → #2111 · back to history
addedTriangle inequality for a metriccf76288de454
addedSymmetry of a metric8243fbb94056
modifiedNon-negativity of a metricf1743900b2c5
| Field | From #1386 | To #2111 |
|---|
| note | `dist_nonneg : 0 ≤ dist x y` is proved at line 251 of `Mathlib/Topology/MetricSpace/Pseudo/Defs.lean`. | `dist_nonneg : 0 ≤ dist x y` is a basic consequence of the (pseudo)metric axioms in `Mathlib/Topology/MetricSpace/Pseudo/Defs.lean`. |
modifiedConvergence of a sequence703805a98984
| Field | From #1386 | To #2111 |
|---|
| mathlib.module | Mathlib.Order.Filter.Basic | Mathlib.Order.Filter.Defs |
addedContinuous function on topological spaces277543c645cb
modifiedDifferential equationa5fbefa41023
| Field | From #1386 | To #2111 |
|---|
| mathlib.module | Mathlib.Analysis.ODE.Gronwall | Mathlib.Analysis.ODE.ExistUnique |
| note | Mathlib's `Mathlib/Analysis/ODE/` formalizes ODE solutions (e.g., Picard–Lindelöf, Gronwall), but there is no general `DifferentialEquation` definition. | Mathlib's `Mathlib/Analysis/ODE/` formalizes ODE solutions (e.g., Picard–Lindelöf uniqueness), but there is no general `DifferentialEquation` definition. |
addedLebesgue measure on Euclidean space70ed1c429cc2
addedσ-algebra of measurable subsetse69b1d68fa23
addedCounting measure1f1afe56e9e0