DomainHeineErgo

Heine-Cantor with a graph defined only on the interval

Open in Workbench View on GitHub

1-- Heine-Cantor with a graph defined only on the interval2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module DomainHeineErgo8import Grace.Cumulus.Real.Analysis910theorem constant_interval_uniform (A B L : Real)11  shows UniformContinuousOnDomain(12    constantFunction(closedInterval(A, B), ℝ, L), closedInterval(A, B))13proof14  have subset := closedInterval.subset_reals at A, B with assumption, assumption15  have continuous := constantFunction.continuous_on_domain at16    closedInterval(A, B), L with subset17  exact closedInterval.heine_cantor_on_domain at18    constantFunction(closedInterval(A, B), ℝ, L), A, B with19      assumption, assumption, continuous20