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 63 research declarations. Search 10,000 more complete Mathlib declarations.
63 results
Clear filtersAutomata.acc_lang_pset
Plain-language statement
The language accepted by M.Pset is the same as that accepted by M, where the accepting states of M.Pset are those that contains at least one accepting state of M.
Source project: Automata Theory
Person-level attribution pending.
Automata.acc_lang_union
Plain-language statement
The language accepted by the sum NA is the union of the languages accepted by the component automata.
Source project: Automata Theory
Person-level attribution pending.
Automata.acc_omega_lang_concat
Plain-language statement
The ω-language of the concatenation NA that is accepted by M1's accepting states is the language accepted by M0 concatenated with the ω-language accepted by M1.
Source project: Automata Theory
Person-level attribution pending.
Automata.acc_omega_lang_inter2
Plain-language statement
The ω-language accepted by the OI2 NA is the intersection of the ω-languages accepted by M0 and M1.
Source project: Automata Theory
Person-level attribution pending.
Automata.acc_omega_lang_loop
Plain-language statement
The ω-language accepted by the loop NA is the ω-power of the language accepted by M.
Source project: Automata Theory
Person-level attribution pending.
Automata.acc_omega_lang_union
Plain-language statement
The ω-language accepted by the sum NA is the union of the ω-languages accepted by the component automata.
Source project: Automata Theory
Person-level attribution pending.