ComplexSequentialContinuity

Continuity preserves sequence limits, entirely in ZF

Open in Workbench View on GitHub

1-- Continuity preserves sequence limits, entirely in ZF.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 ComplexSequentialContinuityExample9import Grace.Cumulus.Complex.SequentialContinuity10theorem maps_limit (f u a : Set)11  requires continuous : ComplexContinuousAt(f, a)12  requires converges : ComplexConvergesTo(u, a)13  shows ComplexConvergesTo(complexMappedSequence(f, u), f(a))14proof15  exact ComplexContinuousAt.converges with *1617theorem polynomial_norm_limit (u a : Set) (cs : List(complexCarrier))18  requires converges : ComplexConvergesTo(u, a)19  shows ConvergesTo(complexNormSequence(complexMappedSequence(complexPolynomial(cs), u)), complexNormSquared(complexPolynomial(cs)(a)))20proof21  exact complexPolynomial.norm_converges with *22