Revision #2666 → #4151 · back to history
modifiedUniformly continuous implies continuous0a43da5de173
| Field | From #2666 | To #4151 |
|---|
| note | Verified at Mathlib/Topology/UniformSpace/Basic.lean line 521. | Verified via decl_exists in Mathlib.Topology.UniformSpace.Basic. |
modifiedImage of totally bounded set0eca0dddbe1f
| Field | From #2666 | To #4151 |
|---|
| note | Stated exactly at line 663 of Cauchy.lean. | Confirmed to exist in Mathlib.Topology.UniformSpace.Cauchy. |
modifiedHeine–Cantor theoreme878539ede14
| Field | From #2666 | To #4151 |
|---|
| note | Heine-Cantor theorem in the uniform-space setting. | Heine–Cantor theorem in the uniform-space setting. |
modifiedLinear functions8f64eeac110a
| Field | From #2666 | To #4151 |
|---|
| mathlib.module | Mathlib.Topology.Algebra.Module.LinearMap | Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic |
modifiedContinuous on compact interval62d6c416751f
| Field | From #2666 | To #4151 |
|---|
| note | Special case of Heine-Cantor applied to a compact subset like [a,b]. | Special case of Heine–Cantor applied to a compact subset like [a,b]. |
modifiedLipschitz and Hölder are uniformly continuousa78602b72e71
| Field | From #2666 | To #4151 |
|---|
| note | Lipschitz case verified at line 188; Hölder case is `HolderWith.uniformContinuous` in Mathlib/Topology/MetricSpace/Holder.lean. | Lipschitz case verified; Hölder case is `HolderWith.uniformContinuous` in Mathlib.Topology.MetricSpace.Holder. |
modifiedAbsolute value function64e567ec5c4e
| Field | From #2666 | To #4151 |
|---|
| note | Verified at line 61 of Real/Lemmas.lean. | Confirmed via decl_exists. |
modifiedUniformly equicontinuous membersd3f0222e9a60
| Field | From #2666 | To #4151 |
|---|
| note | Verified at line 372 of Equicontinuity.lean. | Confirmed via decl_exists. |
modifiedLinear maps: continuous iff uniformly continuousb4213e2b03a4
| Field | From #2666 | To #4151 |
|---|
| mathlib.module | Mathlib.Topology.Algebra.Module.LinearMap | Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic |
modifiedUniform continuity on uniform spaces2ef61335ee1e
| Field | From #2666 | To #4151 |
|---|
| note | Defined at line 807 via uniformity filters (equivalent to the entourage formulation). | Defined via uniformity filters, equivalent to the entourage formulation. |
modifiedUniformly continuous maps preserve Cauchy sequences21c882dd29eb
| Field | From #2666 | To #4151 |
|---|
| note | Verified at line 254 of Cauchy.lean. | Confirmed via decl_exists. |
modifiedGeneralized Heine–Cantor theorem2eac46ae9dd4
| Field | From #2666 | To #4151 |
|---|
| note | Mathlib's Heine-Cantor is already stated in the uniform-space generality. | Mathlib's Heine–Cantor is already stated in the uniform-space generality. |
addedUnbounded function on bounded domain is not uniformly continuousdebdacb5edf7
addedIsometry is uniformly continuous24db14bd9ef5
addedTietze extension theorem (classical statement)d88d6574476d