Skip to content

Consider an alternate definition of continuity #1715

@lowasser

Description

@lowasser

Classical analysis defines the word "continuity" by itself as pointwise continuity.

Bishop, and some other constructive analysis texts I've read, use a different definition of "continuous function" that is classically equivalent, which I'll call local uniform continuity: that a function is uniformly continuous on every closed interval (in the reals), or (in a more general metric space) on every totally bounded subset.

I think we should use this classically equivalent but much more constructively useful definition for the word "continuous," and reserve "pointwise continuous" for the direct translation of the classical definition.

This is at least partially me going, "I absolutely do not want to write locally-uniformly-continuous in practically every function name."

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions