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 685 to 690 of 2,569 results.
Cslib.ωLanguage.IsRegular.compl
Mathematical statement
The complementation of an ω-regular language is ω-regular.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.ωLanguage.IsRegular.eq_fin_iSup_hmul_omegaPow
Mathematical statement
An ω-language is regular iff it 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.ωLanguage.IsRegular.fin_cover_saturates
Mathematical statement
If an ω-language has a finite saturating cover made of ω-regular languages, then it is an ω-regular language.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.ωLanguage.IsRegular.inf
Mathematical statement
The intersection of two ω-regular languages is ω-regular.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.ωLanguage.IsRegular.sup
Mathematical statement
The union of two ω-regular languages is ω-regular.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.ωLanguage.omegaPow_seq_prop
Mathematical statement
An alternative characterization of l^ω.
Source project: Lean Computer Science Library
Person-level attribution pending.