Lax Lean Archive

Words over an ordered alphabet

Lax503819.Words · concepts/Lax503819/Words.lean · lax-503819

definition

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

    Definition

    A word is a finite list of letters, including the empty list. Positions are numbered from zero. The order on words compares words of equal length, letter by letter. A language is monotone if it is upward closed for this order; its upward closure consists of words above one of its members. These are the definitions of Section 2 of Kuperberg (2023).

    Concept map
    1 concept; 5 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Computability.Language
    2import Mathlib.Data.List.Forall2
    3
    4/-!
    5---
    6title: Words over an ordered alphabet
    7type: definition
    8---
    9A word is a finite list of letters, including the empty list. Positions are
    10numbered from zero. The order on words compares words of equal length,
    11letter by letter. A language is monotone if it is upward closed for this
    12order; its upward closure consists of words above one of its members.
    13These are the definitions of Section 2 of Kuperberg (2023).
    14-/
    15
    16namespace Lax503819.Words
    17
    18abbrev Position {A : Type} (w : List A) := Fin w.length
    19
    20def Below {A : Type} [LE A] (u v : List A) : Prop :=
    21 List.Forall₂ (· ≤ ·) u v
    22
    23def MonotoneLanguage {A : Type} [LE A] (L : Language A) : Prop :=
    24 ∀ u v, Below u v → u ∈ L → v ∈ L
    25
    26def upwardClosure {A : Type} [LE A] (L : Language A) : Language A :=
    27 {v | ∃ u ∈ L, Below u v}
    28
    29end Lax503819.Words
    30
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…