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 filtersdet_muller_lang_union
Plain-language statement
Deterministic Muller languages are closed under union.
Source project: Automata Theory
Person-level attribution pending.
frequently_in_finite_set
Plain-language statement
Note that only the → direction needs the finiteness assumption.
Source project: Automata Theory
Person-level attribution pending.
inf_occ_eventually
Plain-language statement
Over a finite type, xs k is in InfOcc xs for all sufficiently large k.
Source project: Automata Theory
Person-level attribution pending.
inf_occ_pair
Plain-language statement
Same as inf_acc_proj, but for pair types. This result does follow from inf_occ_proj, but that proof (see below) turns out to be longer.
Source project: Automata Theory
Person-level attribution pending.
inf_occ_proj
Plain-language statement
Note that only the ⊇ direction needs the finiteness assumptions.
Source project: Automata Theory
Person-level attribution pending.
omega_reg_lang_fin_idx_congr
Plain-language statement
If a congruence is of finite index, is ample, and saturates an ω-language L, then L is ω-regular.
Source project: Automata Theory
Person-level attribution pending.