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 2,569 research declarations. Search 10,000 more complete Mathlib declarations.
2569 results
Automata.greater_subseq_lemma
Project documentation
A technical lemma for use in the next theorem.
Source project: Automata Theory
Person-level attribution pending.
Automata.na_AcceptedLang_of_FinAccept'
Project documentation
The following theorem shows that under the assumption that the alphabet type A is inhabited, the definitions using infinite sequences and those using finite sequences actually define the same notion of the accepted language of an automaton.
Source project: Automata Theory
Person-level attribution pending.
Automata.na_concat_fin_run_0
Plain-language statement
A finite run of the concatenation NA that ends in a state of M0 is completely a run of M0.
Source project: Automata Theory
Person-level attribution pending.
Automata.na_concat_fin_run_1
Plain-language statement
A finite run of the concatenation NA that ends in a state of M1 consists of a run of M0 followed by a run of M1.
Source project: Automata Theory
Person-level attribution pending.
Automata.na_concat_inf_run
Plain-language statement
An infinite run of the concatenation NA that contains a state of M1 consists of a finite run of M0 followed by an infinite run of M1.
Source project: Automata Theory
Person-level attribution pending.
Automata.na_hist_fin_run_exists
Plain-language statement
Any finite run of the original NA can be extended to a finite run of the history NA, assuming that the history component can always "follow along".
Source project: Automata Theory
Person-level attribution pending.