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 63 research declarations. Search 10,000 more complete Mathlib declarations.
63 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.
det_muller_lang_concat
Plain-language statement
The concatenation of a regular language and a deterministic Muller language is a deterministic Muller language.
Source project: Automata Theory
Person-level attribution pending.
det_muller_lang_imp_omega_reg_lang
Plain-language statement
Every deterministic Muller language is an ω-regular language.
Source project: Automata Theory
Person-level attribution pending.
det_muller_lang_inter
Plain-language statement
Deterministic Muller languages are closed under intersection.
Source project: Automata Theory
Person-level attribution pending.