Revision #3397 → #3929 · back to history
modifiedSinc function continuous9422f5f44dd0
| Field | From #3397 | To #3929 |
|---|
| moderation_proposal.fields | {"status":"formalized","mathlib":{"decl":"Real.continuous_sinc","module":"Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc","match_kind":"exact"}} | — |
| moderation_proposal.reason | Verified: `Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc` defines `Real.sinc` and a `continuous_sinc` lemma. | — |
modifiedCoarser/finer comparison of topologiesff44236fff15
| Field | From #3397 | To #3929 |
|---|
| mathlib.decl | TopologicalSpace.instLE | TopologicalSpace.le_def |
| note | The `≤` order on `TopologicalSpace X` formalizes coarser-vs-finer comparison. | The `≤` order on `TopologicalSpace X`, characterized by `TopologicalSpace.le_def`, formalizes coarser-vs-finer comparison. |
addedReciprocal function (example of partial function)38040389594d
addedTangent function (example of partial function)cbd0759de919
addedOscillation of a function at a point4ab1844d8c84
addedLebesgue integrability condition via continuity set540ee048d24e
addedNeighborhood of a point12584ba6f6df
addedContinuous function without maximum on open interval3757b0bb38b3
addedLeft-continuous functione4f40a93a652
addedDirected set0ee8b24ef4f8
addedScott topology9cccae6c4779