Existing in Mathlib · Computability and logic
Myhill–Nerode Theorem
For each possible prefix x, look at exactly which suffixes y complete x to a word in the language. The language is regular exactly when only finitely many different suffix-languages arise as x varies.
- regular languages
- left quotients
- deterministic finite automata
- finite ranges
- formal languages
Exact theorem
Exact Mathlib statement
theorem Language.isRegular_iff_finite_range_leftQuotient {α : Type u} {L : Language α} : L.IsRegular ↔ (Set.range L.leftQuotient).FiniteThe theorem at a glance
Myhill–Nerode theorem at a glance
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Myhill–Nerode theorem at a glance
Detailed visual description
A restrained editorial poster gives the exact left-quotient equivalence in large type, defines the left quotient by the suffix condition x ++ y ∈ L, and uses a small two-way automata-and-quotients diagram without adding minimality, Nerode-index, or pumping-lemma claims.
Statement structure
From hypotheses to conclusion
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
Myhill–Nerode Theorem — scientific diagram
Detailed visual description
This target indexes Mathlib's left-quotient formulation of the Myhill–Nerode theorem. For a language L, leftQuotient sends a word x to the language of suffixes y such that x ++ y ∈ L. The theorem identifies regularity of L with finiteness of the range of that function. It does not, in this declaration, assert uniqueness of a minimal DFA, state finite index of the Nerode equivalence, or derive the pumping lemma.
Why it matters
A mathematical landmark
The theorem gives a structural characterization of regular languages: finite-state recognizability is exactly finiteness of the possible residual languages after prefixes. It is a foundational bridge between automata and language semantics.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This target indexes Mathlib's left-quotient formulation of the Myhill–Nerode theorem. For a language L, leftQuotient sends a word x to the language of suffixes y such that x ++ y ∈ L. The theorem identifies regularity of L with finiteness of the range of that function. It does not, in this declaration, assert uniqueness of a minimal DFA, state finite index of the Nerode equivalence, or derive the pumping lemma.
- Proof Atlas did not originate the Myhill–Nerode theorem or Mathlib's declaration.
- The selected declaration does not state uniqueness or minimality of a DFA.
- The selected declaration is not phrased as finiteness of the index of the Nerode equivalence.
- The selected declaration does not state or prove the pumping lemma.
- The generated explanation and visuals are not proof evidence.
Source and local evidence
Where the theorem comes from
- Existing declaration
Language.isRegular_iff_finite_range_leftQuotientin mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.myhill-nerode-theorem.v001