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 filtersCslib.Automata.NA.concat_run_proj
Plain-language statement
A run of concat na1 na2 containing at least one na2 state is the concatenation of an accepting finite run of na1 followed by a run of na2.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.FinAcc.finConcat_language_eq
Plain-language statement
finConcat na1 na2 accepts the concatenation of the languages of na1 and na2.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.FinAcc.loop_language_eq
Plain-language statement
finLoop na accepts the Kleene star of the language of na, assuming that the latter is nonempty.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.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.