Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 4 research declarations. Search 10,000 more complete Mathlib declarations.
4 results
Clear filtersCslib.Automata.DA.FinAcc.unique_minimal
Plain-language statement
The minimal DFA M accepting the language l is unique up to unique isomorphism.
Source project: Lean Computer Science Library
Person-level attribution pending.
Language.dfa_num_state_ge
Plain-language statement
Given a set of strings all distinguishable by l (i.e., not related to each other by the Nerode congruence on l), the number of states in the DFA accepting l is at least the number of strings in the set.
Source project: Lean Computer Science Library
Person-level attribution pending.
Language.dfa_num_state_min
Plain-language statement
All DFAs accepting l must have at least as many states as the number of equivalence classes of the Nerode congruence on l.
Source project: Lean Computer Science Library
Person-level attribution pending.
Language.IsRegular.finite_nerodeQuotient
Plain-language statement
If l is regular then the Nerode congruence on l has finitely many equivalence classes.
Source project: Lean Computer Science Library
Person-level attribution pending.