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 filtersAutomata.buchi_congr_ample
Project documentation
The BuchiCongr of an NA is ample if the NA is finite-state. For simplicity, this result is proved using a Ramsey theorem on infinite graphs.
Source project: Automata Theory
Person-level attribution pending.
Automata.buchi_congr_saturates
Plain-language statement
The BuchiCongr of an NA saturates the ω-language accepted by the NA. Note that this result does not need to assume that the NA is finite-state.
Source project: Automata Theory
Person-level attribution pending.
Automata.choueka_lang_decomp_lemma
Plain-language statement
The following lemmas are used to prove that the Choueka language is regular.
Source project: Automata Theory
Person-level attribution pending.
Automata.choueka_lang_omega_limit_subset_omega_power
Project documentation
The ω-limit of the Choueka language of M is a subset of the ω-power of the language of M. Note that this theorem does not need to assume that M is finite-state.
Source project: Automata Theory
Person-level attribution pending.
Automata.choueka_lang_omega_power_eq_omega_limit
Project documentation
If the language accepted by M is of the form V∗, then V^ω = V∗ * (M.ChouekaLang acc)↗ω. Note that this theorem does need to assume that M is finite-state.
Source project: Automata Theory
Person-level attribution pending.
Automata.choueka_lang_omega_power_subset_omega_limit
Project documentation
If the language accepted by M is of the form V∗, then V^ω ⊆ V∗ * (M.ChouekaLang acc)↗ω. Note that this theorem does need to assume that M is finite-state.
Source project: Automata Theory
Person-level attribution pending.