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 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 577 to 582 of 2,569 results.
Cslib.Automata.NA.concat_run_exists
Mathematical statement
Given an accepting finite run of na1 and a run of na2, there exists a run of concat na1 na2 that is the concatenation of the two runs.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.concat_run_proj
Mathematical 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
Mathematical 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
Mathematical 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
Mathematical 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
Mathematical 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.