Lax Lean Archive

Rational relations are continuous

Lax132576.RationalContinuity · 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.

    Natural Language Statement

    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.

    Concept map
    4 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    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

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…