Revision #1792 → #2293 · back to history
modifiedMetric topology equals order topology144a7732bcbd
| Field | From #1792 | To #2293 |
|---|
| mathlib.decl | — | instOrderTopologyReal |
| mathlib.match_kind | exact | invocation |
| note | The `instance : OrderTopology ℝ` establishes that the order topology coincides with ℝ's metric-induced topology. | The `instOrderTopologyReal : OrderTopology ℝ` instance combined with ℝ's metric structure establishes that ℝ's order and metric topologies coincide. |
| provenance | ai | ai-moderated |
modifiedAbsolute continuity965ccf380227
| Field | From #1792 | To #2293 |
|---|
| mathlib.decl | AbsolutelyContinuousOnInterval | — |
| mathlib.match_kind | exact | — |
| mathlib.module | Mathlib.MeasureTheory.Function.AbsolutelyContinuous | — |
| note | AbsolutelyContinuousOnInterval formalizes absolute continuity of a function on an interval, with the ε-δ form in absolutelyContinuousOnInterval_iff. | Mathlib has `MeasureTheory.Measure.AbsolutelyContinuous` for measures, but absolute continuity of a function on an interval is not yet a named Mathlib definition. |
| provenance | ai | ai-moderated |
| status | formalized | partial |
modifiedAbsolutely continuous implies continuous7a0c89b42844
| Field | From #1792 | To #2293 |
|---|
| mathlib.decl | AbsolutelyContinuousOnInterval.uniformContinuousOn | — |
| mathlib.match_kind | generalization | — |
| mathlib.module | Mathlib.MeasureTheory.Function.AbsolutelyContinuous | — |
| note | AbsolutelyContinuousOnInterval.uniformContinuousOn proves absolutely continuous functions are uniformly (hence) continuous. | Without a named definition of absolutely continuous functions on intervals, the corollary that they are continuous is not a single named Mathlib lemma. |
| provenance | ai | ai-moderated |
| status | formalized | partial |
addedOrdered field structure on ℝe2e4597bc97f
addedTotal order on ℝb4af2c647ba6
addedOpen cover785162ca4e69
addedBanach space0e1ebca434ff
addedHilbert spacebf27688af062
addedExtended real linefc0fea9b7c41
addedHolomorphic function613a23904cd0