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,369 to 1,374 of 2,569 results.
inf_occ_eventually
Mathematical 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
Mathematical 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
Mathematical statement
Note that only the ⊇ direction needs the finiteness assumptions.
Source project: Automata Theory
Person-level attribution pending.
InfClosed.mem_countableInfClosure_iff
Mathematical statement
If the set is inf-closed, elements of countablInfClosure can be written as countable intersections of antitone sequences of sets.
Source project: Brownian motion
Person-level attribution pending.
InfModel.Equation374794_not_implies_Equation2
Mathematical statement
However, Equation374794 doesn't imply Equation2.
Source project: Equational Theories
Person-level attribution pending.
InfModel.Finite.Equation374794_implies_Equation2
Mathematical statement
In a finite model Equation374794 implies Equation2, that the model is a subsingleton.
Source project: Equational Theories
Person-level attribution pending.