Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Expressive completeness

Lax149335.ExpressiveCompleteness · concepts/Lax149335/ExpressiveCompleteness.lean · lax-149335

open

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

    Theorem 3.2 (Expressive completeness). A function between types is rational if and only if it is the denotation of some rational term.

    This theorem is not proved in this submission; it is recorded as an open statement. Nothing else in the submission depends on it.

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

    Each proof establishes this claim relative to its assumptions.

    No proof in the archive yet — this claim is open.

    Lean source view on GitHub

    1import Lax149335.RationalFunctions
    2import Lax149335.Terms
    3
    4/-!
    5---
    6title: Expressive completeness
    7type: theorem
    8---
    9**Theorem 3.2 (Expressive completeness).** A function between types is rational if and only
    10if it is the denotation of some rational term.
    11
    12This theorem is not proved in this submission; it is recorded as an open statement. Nothing
    13else in the submission depends on it.
    14-/
    15
    16namespace Lax149335.ExpressiveCompleteness
    17
    18open Lax149335.Types Lax149335.RationalFunctions Lax149335.Terms
    19
    20/-- **Theorem 3.2.** A function between types is rational if and only if it is the denotation
    21of some rational term. -/
    22axiom expressive_completeness {A B : Ty} (f : ⟦A⟧ → ⟦B⟧) :
    23 IsRationalTypeFun f ↔ ∃ t : Term A B, t.den = f
    24
    25end Lax149335.ExpressiveCompleteness
    26
    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…