Lax Lean Archive

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

Lax132576.RationalContinuity

Rational relations are continuous

concepts/Lax132576/RationalContinuity.lean · lax-132576

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

    If R⊆A∗×B∗R \subseteq A^* \times B^* is a rational relation and L⊆B∗L \subseteq B^* is a regular language, then the inverse image

    {w∈A∗∣w R v for some v∈L}\{w \in A^* \mid w\,R\,v \text{ for some } v \in L\}

    is a regular language (Theorem B.1.5 of Transducers). The book deduces it from closure under composition: rational relations with an empty output alphabet are the regular languages over the input alphabet, and the inverse image is the composition of RR with the relation {(w,ε)∣w∈L}\{(w, \varepsilon) \mid w \in L\}. Since rational relations are input/output symmetric, forward images of regular languages are regular too.

    Lean source view on GitHub

    1import Lax765601.Continuity
    2import Lax132576.RationalRelations
    3
    4/-!
    5---
    6title: Rational relations are continuous
    7type: theorem
    8---
    9If R⊆A∗×B∗R \subseteq A^* \times B^* is a rational relation and L⊆B∗L \subseteq B^*
    10is a regular language, then the inverse image
    11{w∈A∗∣w R v for some v∈L}\{w \in A^* \mid w\,R\,v \text{ for some } v \in L\}
    12is a regular language (Theorem B.1.5 of *Transducers*). The book deduces it
    13from closure under composition: rational relations with an empty output
    14alphabet are the regular languages over the input alphabet, and the inverse
    15image is the composition of RR with the relation {(w,ε)∣w∈L}\{(w, \varepsilon) \mid w \in L\}.
    16Since rational relations are input/output symmetric, forward images of regular
    17languages are regular too.
    18
    19# Formalization notes
    20
    21The conclusion is `RelContinuous R` of `Lax765601.Continuity`, continuity in
    22the relational form. No finiteness of the alphabets is needed.
    23-/
    24
    25namespace Lax132576.RationalContinuity
    26
    27open Lax765601.Continuity Lax132576.RationalRelations
    28
    29/-- A rational relation is continuous: inverse images of regular languages are
    30regular. -/
    31axiom relContinuous_of_isRationalRel {A B : Type} {R : List A → List B → Prop}
    32 (hR : IsRationalRel R) : RelContinuous R
    33
    34end Lax132576.RationalContinuity
    35
    Show Proof

    Formalization notes

    The conclusion is RelContinuousRRelContinuous R of Lax765601.ContinuityLax765601.Continuity, continuity in the relational form. No finiteness of the alphabets is needed.

    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…