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 571 to 576 of 2,569 results.
Cslib.Automata.NA.Buchi.buchiFamily_saturation
Mathematical 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
Mathematical 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
Mathematical 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
Mathematical 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.
Cslib.Automata.NA.Buchi.inter_language_eq
Mathematical 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
Mathematical 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.