Grace/Cumulus/Metric.g17

Open in Workbench Download source

Imports

Space · Ball · Open · Closed · Continuity · Sequences · Bounded · Uniform · Line · Discrete · Subspace · Product · Limits · Maps · Structure · Spaces

Declarations

Source

1-- Metric spaces: distance functions, balls, the metric topology, closed2-- sets, continuity, sequences and completeness, bounded sets, uniform3-- continuity, the real line, discrete, subspace, and product metrics,4-- limits, and Lipschitz maps and isometries5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Metric11import Space12import Ball13import Open14import Closed15import Continuity16import Sequences17import Bounded18import Uniform19import Line20import Discrete21import Subspace22import Product23import Limits24import Maps25import Structure26import Spaces27