ComplexCompactness

Compactness clients: no coordinate bookkeeping at the point of use

Open in Workbench View on GitHub

1-- Compactness clients: no coordinate bookkeeping at the point of use.2-- 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 Passmore67-- Copyright (c) 2026 Grant Passmore. Apache License 2.0.8module ComplexCompactnessExample9import Grace.Cumulus.Complex.Compactness10theorem disk_compact (radius : Real)11  shows ComplexSequentiallyCompact(closedComplexDisk(radius))12proof13  exact closedComplexDisk.sequentially_compact with *1415theorem extract (u : Set) (radius : Real)16  requires sequence : ComplexSequence(u)17  requires terms : TermsIn(u, closedComplexDisk(radius))18  shows ∃ k, StrictlyIncreasingNat(k) ∧ ∃ a ∈ closedComplexDisk(radius),19    ComplexConvergesTo(complexSubsequence(u, k), a)20proof21  exact closedComplexDisk.bolzano_weierstrass with *2223theorem norm_limit (u a : Set)24  requires converges : ComplexConvergesTo(u, a)25  shows ConvergesTo(complexNormSequence(u), complexNormSquared(a))26proof27  exact ComplexConvergesTo.norm_squared with *2829theorem coordinate_bound (a radius : Real)30  requires squareBound : a * a ≤ radius31  shows -(radius + 1) ≤ a ∧ a ≤ radius + 132proof33  exact realSquare.coordinate_bounds with *34