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.DA.FinAcc.unique_minimal
Plain-language statement
The minimal DFA M accepting the language l is unique up to unique isomorphism.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.Buchi.buchiFamily_cover
Project documentation
na.buchiFamily is a cover if na has only finitely many states. This theorem uses the Ramsey theorem for infinite graphs and does not depend on any details of na.BuchiCongruence other than that it is of finite index.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.Buchi.buchiFamily_saturation
Plain-language statement
na.buchiFamily saturates the ω-language accepted by na.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.Buchi.concat_language_eq
Plain-language statement
The Buchi automaton formed from concat na1 na2 accepts the ω-language that is the concatenation of the language of na1 and the ω-language of na2.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.Buchi.inter_freq_acc_freq_acc
Plain-language statement
If the intersection automaton sees one accepting condition infinitely many times, then it sees the other accepting condition infinitely many times as well.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.Buchi.inter_freq_comp_acc_freq_acc
Plain-language statement
If the intersection automaton sees the accepting conditions of both component automata infinitely many times, then its own accepting condition also happens infinitely many times.
Source project: Lean Computer Science Library
Person-level attribution pending.