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.Buchi.inter_language_eq
Plain-language statement
The language accepted by the intersection automaton is the intersection of the languages accepted by the two component automata.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.Buchi.language_eq_fin_iSup_hmul_omegaPow
Plain-language statement
The ω-language accepted by a finite-state Büchi automaton is the finite union of ω-languages of the form L * M^ω, where all Ls and Ms are regular languages.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.concat_run_exists
Plain-language 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
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.