Revision #2913 → #3397 · back to history
modifiedContinuity at a point via limitsb7ead4649129
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Definition in terms of limits of functions","snippet":"The function f is continuous at some point c of its domain if the limit of"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{x\\to c}{f(x)}=f(c).}"}] | — |
modifiedContinuity via sequencesbc866546bf21
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Definition in terms of limits of sequences","snippet":"One can instead require that for any sequence"},{"type":"math_alttext","value":"{\\displaystyle \\forall (x_{n})_{n\\in \\mathbb {N} }\\subset D:\\lim _{n\\to \\infty }x_{n}=c\\Rightarrow \\lim _{n\\to \\infty }f(x_{n})=f(c)\\,.}"}] | — |
modifiedEpsilon–delta continuity570a69d81d5f
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Weierstrass and Jordan definitions (epsilon–delta) of continuous functions","snippet":"is said to be continuous at the point"},{"type":"math_alttext","value":"{\\displaystyle f\\left(x_{0}\\right)-\\varepsilon <f(x)<f(x_{0})+\\varepsilon .}"}] | — |
modifiedC-continuous at a pointfbcabb4e5d0f
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Definition in terms of control of the remainder","snippet":"is C -continuous at"},{"type":"math_alttext","value":"{\\displaystyle |f(x)-f(x_{0})|\\leq C\\left(\\left|x-x_{0}\\right|\\right){\\text{ for all }}x\\in D\\cap N(x_{0})}"}] | — |
modifiedSinc function continuous9422f5f44dd0
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Rules for continuity","snippet":"An example of a function for which the above rules are not sufficient is the sinc function"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{x\\to 0}{\\frac {\\sin x}{x}}=1.}"}] | — |
| mathlib.decl | — | Real.continuous_sinc |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc |
| 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. |
| note | No `sinc` function appears to be defined in Mathlib. | Mathlib defines `Real.sinc` in `Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc` with a `continuous_sinc` lemma showing it is continuous everywhere. |
| status | not_formalized | formalized |
modifiedHeaviside step function6e984c9e5cf3
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Examples of discontinuous functions","snippet":"An example of a discontinuous function is the Heaviside step function"},{"type":"math_alttext","value":"{\\displaystyle H(x)={\\begin{cases}1&{\\text{ if }}x\\geq 0\\\\0&{\\text{ if }}x<0\\end{cases}}}"}] | — |
modifiedSignum function discontinuous at 0f7dd3d173c5e
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Examples of discontinuous functions","snippet":"the signum or sign function"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {sgn}(x)={\\begin{cases}\\;\\;\\ 1&{\\text{ if }}x>0\\\\\\;\\;\\ 0&{\\text{ if }}x=0\\\\-1&{\\text{ if }}x<0\\end{cases}}}"},{"type":"math_alttext","value":"{\\displaystyle f(x)={\\begin{cases}\\sin \\left(x^{-2}\\right)&{\\text{ if }}x\\neq 0\\\\0&{\\text{ if }}x=0\\end{cases}}}"}] | — |
modifiedDirichlet's function nowhere continuous7ab0404ee622
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Examples of discontinuous functions","snippet":"Dirichlet's function , the indicator function for the set of rational numbers"},{"type":"math_alttext","value":"{\\displaystyle f(x)={\\begin{cases}1&{\\text{ if }}x=0\\\\{\\frac {1}{q}}&{\\text{ if }}x={\\frac {p}{q}}{\\text{(in lowest terms) is a rational number}}\\\\0&{\\text{ if }}x{\\text{ is irrational}}.\\end{cases}}}"},{"type":"math_alttext","value":"{\\displaystyle D(x)={\\begin{cases}0&{\\text{ if }}x{\\text{ is irrational }}(\\in \\mathbb {R} \\setminus \\mathbb {Q} )\\\\1&{\\text{ if }}x{\\text{ is rational }}(\\in \\mathbb {Q} )\\end{cases}}}"}] | — |
modifiedDifferentiable implies continuous6e7db5aec80e
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Relation to differentiability and integrability","snippet":"Every differentiable function"},{"type":"math_alttext","value":"{\\displaystyle f:(a,b)\\to \\mathbb {R} }"}] | — |
modifiedAbsolute value continuous but not differentiable at 0312f4e51cf4f
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Relation to differentiability and integrability","snippet":"the absolute value function"},{"type":"math_alttext","value":"{\\displaystyle f:(a,b)\\to \\mathbb {R} }"}] | — |
modifiedContinuously differentiable / C^k class25b508d383db
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Relation to differentiability and integrability","snippet":"If f′ ( x ) is continuous, f ( x ) is said to be continuously differentiable"},{"type":"math_alttext","value":"{\\displaystyle f:\\Omega \\to \\mathbb {R} }"}] | — |
modifiedContinuous functions are integrableac6aa8971240
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Relation to differentiability and integrability","snippet":"Every continuous function"},{"type":"math_alttext","value":"{\\displaystyle f:[a,b]\\to \\mathbb {R} }"}] | — |
modifiedPointwise limit of functions29e1461c6349
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Pointwise and uniform limits","snippet":"the resulting function"},{"type":"math_alttext","value":"{\\displaystyle f_{1},f_{2},\\dotsc :I\\to \\mathbb {R} }"},{"type":"math_alttext","value":"{\\displaystyle f(x):=\\lim _{n\\to \\infty }f_{n}(x)}"}] | — |
modifiedUniform convergence theorem66952e8bf49c
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Pointwise and uniform limits","snippet":"f is continuous if all functions"},{"type":"math_alttext","value":"{\\displaystyle f_{1},f_{2},\\dotsc :I\\to \\mathbb {R} }"},{"type":"math_alttext","value":"{\\displaystyle f(x):=\\lim _{n\\to \\infty }f_{n}(x)}"}] | — |
modifiedRight-continuous functionb387c0a274c9
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Directional Continuity","snippet":"f is said to be right-continuous at the point c if the following holds"},{"type":"math_alttext","value":"{\\displaystyle |f(x)-f(c)|<\\varepsilon }"}] | — |
modifiedLower semi-continuity51812a6de0c4
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Semicontinuity","snippet":"A function f is lower semi-continuous at the point c if, roughly, any jumps that might occur only go down"},{"type":"math_alttext","value":"{\\displaystyle f(x)\\geq f(c)-\\varepsilon .}"}] | — |
modifiedContinuity between metric spacesf4bc5f8d6a9e
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Continuous functions between metric spaces","snippet":"is continuous at the point"},{"type":"math_alttext","value":"{\\displaystyle d_{X}:X\\times X\\to \\mathbb {R} }"},{"type":"math_alttext","value":"{\\displaystyle f:X\\to Y}"}] | — |
modifiedLinear operator continuous iff boundedcb7e1efb401e
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Continuous functions between metric spaces","snippet":"a linear operator"},{"type":"math_alttext","value":"{\\displaystyle T:V\\to W}"},{"type":"math_alttext","value":"{\\displaystyle \\|T(x)\\|\\leq K\\|x\\|}"}] | — |
modifiedHölder continuity9a97b5362753
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Uniform, Hölder and Lipschitz continuity","snippet":"A function is Hölder continuous with exponent α"},{"type":"math_alttext","value":"{\\displaystyle d_{Y}(f(b),f(c))\\leq K\\cdot (d_{X}(b,c))^{\\alpha }}"},{"type":"math_alttext","value":"{\\displaystyle d_{Y}(f(b),f(c))\\leq K\\cdot d_{X}(b,c)}"}] | — |
modifiedLipschitz continuityd59c7b29195d
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Uniform, Hölder and Lipschitz continuity","snippet":"a function is Lipschitz continuous if there is a constant K"},{"type":"math_alttext","value":"{\\displaystyle d_{Y}(f(b),f(c))\\leq K\\cdot (d_{X}(b,c))^{\\alpha }}"},{"type":"math_alttext","value":"{\\displaystyle d_{Y}(f(b),f(c))\\leq K\\cdot d_{X}(b,c)}"}] | — |
modifiedContinuity between topological spaces3116b01d5d20
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Continuous functions between topological spaces","snippet":"between two topological spaces X and Y is continuous if for every open set"},{"type":"math_alttext","value":"{\\displaystyle f:X\\to Y}"},{"type":"math_alttext","value":"{\\displaystyle f^{-1}(V)=\\{x\\in X\\;|\\;f(x)\\in V\\}}"}] | — |
modifiedDiscrete topology makes all maps continuousd4492c505e5b
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Continuous functions between topological spaces","snippet":"if a set X is given the discrete topology"},{"type":"math_alttext","value":"{\\displaystyle f:X\\to T}"}] | — |
modifiedContinuous iff continuous at every point7449a398647d
| Field | From #2913 | To #3397 |
|---|
| anchor.snippet | a function | is continuous at every point of X if and only if it is a continuous function |
| provenance | ai | ai-moderated |
modifiedFilter characterization of continuity at a point536bfde24186
| Field | From #2913 | To #3397 |
|---|
| anchor.snippet | is continuous at | is a filter base for the neighborhood filter |
| provenance | ai | ai-moderated |
modifiedFinal topologyb657b4c11fc7
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Defining topologies via continuous functions","snippet":"the final topology on S is defined by letting the open sets of S be those subsets A of S"},{"type":"math_alttext","value":"{\\displaystyle f:X\\to S,}"}] | — |
modifiedContinuous functorfb7fbad22cf7
| Field | From #2913 | To #3397 |
|---|
| anchors | [{"section":"Related notions","snippet":"a functor"},{"type":"math_alttext","value":"{\\displaystyle F:{\\mathcal {C}}\\to {\\mathcal {D}}}"},{"type":"math_alttext","value":"{\\displaystyle \\varprojlim _{i\\in I}F(C_{i})\\cong F\\left(\\varprojlim _{i\\in I}C_{i}\\right)}"}] | — |
modifiedSequential continuity implies continuity in first-countable spaces87a497831640
| Field | From #2913 | To #3397 |
|---|
| anchor.snippet | If | any function preserving sequential limits is continuous |
| provenance | ai | ai-moderated |
addedConstant function is continuous34090e038799
addedIdentity function is continuous19cbade2d547
addedCauchy-sequence characterization of continuity between metric spacesa254bc0fc3fd
addedCoarser/finer comparison of topologiesff44236fff15