Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax916827.RegularContinuity

Regular functions are continuous

concepts/Lax916827/RegularContinuity.lean · lax-916827

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    Theorem

    Regular functions are continuous (Theorem C.1.1 of Transducers, the continuity half). Continuous functions are closed under composition and rational functions are continuous (Theorem B.1.5), so it remains to see that map reverse and map duplicate are continuous, which is Lemma C.1.2 (reversal and duplication are continuous) lifted through Lemma C.1.3 (the map lifting of a continuous function is continuous).

    Lean source view on GitHub

    1import Lax765601.Continuity
    2import Lax916827.RegularFunctions
    3
    4/-!
    5---
    6title: Regular functions are continuous
    7type: theorem
    8---
    9Regular functions are continuous (Theorem C.1.1 of *Transducers*, the
    10continuity half). Continuous functions are closed under composition and
    11rational functions are continuous (Theorem B.1.5), so it remains to see that
    12map reverse and map duplicate are continuous, which is Lemma C.1.2 (reversal
    13and duplication are continuous) lifted through Lemma C.1.3 (the map lifting of
    14a continuous function is continuous).
    15
    16# Formalization notes
    17
    18The finiteness hypotheses on the alphabets are those of the book; the prime
    19regular functions are in fact continuous over any alphabets.
    20-/
    21
    22namespace Lax916827.RegularContinuity
    23
    24open Lax765601.Continuity Lax916827.RegularFunctions
    25
    26/-- A regular function is continuous. -/
    27axiom continuous_of_isRegularFun {A B : Type} [Finite A] [Finite B] {f : List A → List B}
    28 (hf : IsRegularFun f) : Continuous f
    29
    30end Lax916827.RegularContinuity
    31
    Show Proof

    Formalization notes

    The finiteness hypotheses on the alphabets are those of the book; the prime regular functions are in fact continuous over any alphabets.

    Builds on

    Used by

    none

    From Mathlib

    none

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…