Revision #1321 → #2030 · back to history
modifiedEndpoints of an intervaledd0199958a4
| Field | From #1321 | To #2030 |
|---|
| mathlib.decl | Set.sSup_Icc | csSup_Icc |
| mathlib.module | Mathlib.Order.CompleteLatticeIntervals | Mathlib.Order.ConditionallyCompletePartialOrder.Basic |
| note | No standalone 'endpoint' notion; sup/inf of an interval are computed lemma-by-lemma (e.g. `sSup_Icc`, `csInf_Ioo`). | No standalone 'endpoint' notion; sup/inf of an interval are computed lemma-by-lemma (e.g. `csSup_Icc`, `csInf_Ioo`). |
modifiedLeft/right-bounded interval520fd5beec7d
| Field | From #1321 | To #2030 |
|---|
| mathlib.module | Mathlib.Order.Bounds.Basic | Mathlib.Order.Bounds.Defs |
modifiedLeft/right-open by min/max662b6b3e59b5
| Field | From #1321 | To #2030 |
|---|
| mathlib.module | Mathlib.Order.Bounds.Basic | Mathlib.Order.Bounds.Defs |
modifiedLeft/right-closed interval96ece20aef97
| Field | From #1321 | To #2030 |
|---|
| mathlib.module | Mathlib.Order.Bounds.Basic | Mathlib.Order.Bounds.Defs |
modifiedOpen and closed balls on the real lineac38a14eb2e6
| Field | From #1321 | To #2030 |
|---|
| mathlib.module | Mathlib.Analysis.Normed.Order.Lattice | Mathlib.Topology.MetricSpace.Pseudo.Defs |
modifiedContinuity (epsilon-delta)7e8841f06676
| Field | From #1321 | To #2030 |
|---|
| mathlib.module | Mathlib.Topology.MetricSpace.Basic | Mathlib.Topology.MetricSpace.Pseudo.Defs |
modifiedOrder topology is completely normal11ca94c55d7d
| Field | From #1321 | To #2030 |
|---|
| label | Totally ordered set is monotonically normal | Order topology is completely normal |
| note | `OrderTopology.completelyNormalSpace` (and `t5Space`) prove a linearly ordered space with the order topology is completely normal. | `OrderTopology.completelyNormalSpace` (and `t5Space`) prove a linearly ordered space with the order topology is completely normal. (The article also asserts the stronger 'monotonically normal' result, which is not in Mathlib.) |
| provenance | ai | ai-moderated |
modifiedOpen/closed ball as interval909facc7ee07
| Field | From #1321 | To #2030 |
|---|
| mathlib.module | Mathlib.Analysis.Normed.Order.Lattice | Mathlib.Topology.MetricSpace.Pseudo.Defs |
addedInteger intervalc69f947a837c
addedImage of an interval under a continuous function is an intervaldb74b4c5f812
addedExtended-real interval20f86fa161f7