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 1,789 to 1,794 of 2,569 results.
omega_reg_lang_iff_finite_union_form
Mathematical statement
An ω-language is ω-regular if and only if it is the finite union of sets of the form U * V^ω, where all Us and Vs are regular languages.
Source project: Automata Theory
Person-level attribution pending.
omega_reg_lang_imp_det_muller_lang
Mathematical statement
Every deterministic Muller language is an ω-regular language.
Source project: Automata Theory
Person-level attribution pending.
omega_reg_lang_inter
Mathematical statement
ω-regular languages are closed under intersection.
Source project: Automata Theory
Person-level attribution pending.
omega_reg_lang_union
Mathematical statement
ω-regular languages are closed under union.
Source project: Automata Theory
Person-level attribution pending.
oneJetBundle_chart_source
Mathematical statement
In J¹(M, M'), the source of a chart has a nice formula
Source project: Sphere eversion
Person-level attribution pending.
oneJetBundle_chart_target
Mathematical statement
In J¹(M, M'), the target of a chart has a nice formula
Source project: Sphere eversion
Person-level attribution pending.