Revision #1116 → #1728 · back to history
addedEpsilon–delta definition of a limitc7fa92c65398
addedUniform continuity (concept)bca39215627e
addedScott continuity (concept)7e35ec29c4fa
addedMicrocontinuity (nonstandard)642b2b08c0c5
modifiedReal-valued function on integers is continuousd8280f703086
| Field | From #1116 | To #1728 |
|---|
| mathlib.module | Mathlib.Topology.Defs.Basic | Mathlib.Topology.Order |
modifiedContinuity via oscillation92c1966fc1e0
| Field | From #1116 | To #1728 |
|---|
| mathlib.decl | oscillation_eq_zero | Oscillation.eq_zero_iff_continuousAt |
| note | `oscillation_eq_zero` characterizes continuity at a point by vanishing oscillation. | `Oscillation.eq_zero_iff_continuousAt` characterizes continuity at a point by vanishing oscillation. |
addedContinuity of sine and cosinee660e636cdaf
addedContinuity of exponential function16db4853eaca
addedContinuity of natural logarithm on positive realsb3769e211849
modifiedSignum function discontinuous at 0f7dd3d173c5e
| Field | From #1116 | To #1728 |
|---|
| mathlib.module | Mathlib.Topology.Instances.Sign | Mathlib.Data.Sign.Defs |
modifiedUseful lemma on local sign preservationcd0adada8d90
| Field | From #1116 | To #1728 |
|---|
| mathlib.module | Mathlib.Topology.ContinuousOn | Mathlib.Topology.Continuous |
modifiedContinuous functions are integrableac6aa8971240
| Field | From #1116 | To #1728 |
|---|
| mathlib.module | Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus | Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic |
modifiedUniform convergence theorem66952e8bf49c
| Field | From #1116 | To #1728 |
|---|
| mathlib.module | Mathlib.Topology.UniformSpace.UniformConvergence | Mathlib.Topology.UniformSpace.UniformApproximation |
addedUpper semi-continuityd390d80c5c94
addedMetric spacebc7cf26c5dfc
modifiedContinuity points form a G-delta setf17dd24c93b1
| Field | From #1116 | To #1728 |
|---|
| mathlib.decl | oscillation_eq_zero | Oscillation.eq_zero_iff_continuousAt |
| note | Mathlib has the oscillation infrastructure to express this, but I did not find a direct named lemma asserting the continuity set is `IsGδ`. | Mathlib has the oscillation/continuity characterization, but I did not find a direct named lemma asserting the continuity set is `IsGδ`. |
addedContinuous on compact implies uniformly continuousd134fdf39cde
addedTopological spacefa1d976a1b17
modifiedDiscrete topology makes all maps continuousd4492c505e5b
| Field | From #1116 | To #1728 |
|---|
| mathlib.module | Mathlib.Topology.Defs.Basic | Mathlib.Topology.Order |
addedSequential space22d7455915f7
addedKuratowski closure axiomsb41f82b34458
modifiedContinuous image of separable is separablea1b1fbf21e61
| Field | From #1116 | To #1728 |
|---|
| mathlib.decl | IsSeparable.image | TopologicalSpace.IsSeparable.image |
| note | `IsSeparable.image` formalizes this property. | `TopologicalSpace.IsSeparable.image` formalizes this property. |
modifiedFinal topologyb657b4c11fc7
| Field | From #1116 | To #1728 |
|---|
| mathlib.module | Mathlib.Topology.Order | Mathlib.Topology.Defs.Induced |
addedQuotient topology (as final topology of surjection)93332c68ab08
modifiedInitial topology8ce48247e843
| Field | From #1116 | To #1728 |
|---|
| mathlib.module | Mathlib.Topology.Order | Mathlib.Topology.Defs.Induced |
addedTietze extension theoremaa6c382e1ac5
addedHahn–Banach theoremf97718a7985d