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 199 research declarations. Search 10,000 more complete Mathlib declarations.
199 results
Clear filtersAutomata.pair_acc_lang_regular
Plain-language statement
If M is finite-state, then M.PairAccLang acc s s' is regular for any pair of states s and s'. Note that we need to use the history NA construction to prove this result, because the NA needs to remember whether an accepting state has been visited.
Source project: Automata Theory
Person-level attribution pending.
Automata.pair_lang_regular
Plain-language statement
If M is finite-state, then M.PairLang s s' is regular for any pair of states s and s'.
Source project: Automata Theory
Person-level attribution pending.
Automata.ramsey_lemma
Project documentation
This lemma derives a form of the Ramsey theorem suitable for use in the next theorem.
Source project: Automata Theory
Person-level attribution pending.
Cslib.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.
Cslib.Automata.NA.Buchi.buchiFamily_cover
Project documentation
na.buchiFamily is a cover if na has only finitely many states. This theorem uses the Ramsey theorem for infinite graphs and does not depend on any details of na.BuchiCongruence other than that it is of finite index.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.Buchi.buchiFamily_saturation
Plain-language statement
na.buchiFamily saturates the ω-language accepted by na.
Source project: Lean Computer Science Library
Person-level attribution pending.