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 136 research declarations. Search 10,000 more complete Mathlib declarations.
136 results
Clear filtersCslib.Automata.NA.iProd_run_iff
Plain-language statement
Every run of the product automaton projects onto runs of its component automata, and vice versa.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.iSum_run_iff
Plain-language statement
An infinite run of the sum automaton is an infinite run of one of its component automata.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.loop_run_exists
Plain-language statement
For any infinite sequence xls of nonempty finite words from language na, there is an infinite run of na.loop corresponding to xls.flatten in which the state () marks the boundaries between the finite words in xls.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.loop_run_one_iter
Plain-language statement
A run of na.loop containing at least one non-initial () state is the concatenation of a nonempty finite run of na followed by a run of na.loop.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.totalize_run_mtr
Plain-language statement
In an infinite execution of NA.totalize, as long as the NA stays in a non-sink state, the execution so far corresponds to a finite execution of the original NA.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.εNA.FinAcc.toNAFinAcc_language_eq
Plain-language statement
Correctness of toNAFinAcc.
Source project: Lean Computer Science Library
Person-level attribution pending.