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 691 to 696 of 2,569 results.
Cslib.ωSequence.cons_flatten
Mathematical statement
ls.flatten equals the concatenation of ls.head and ls.tail.flatten.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.ωSequence.frequently_in_finite_type
Mathematical statement
In a finite type, the elements of a set occurs infinitely often iff some element in the set occurs infinitely often.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.ωSequence.frequently_in_strictMono
Mathematical statement
If p is true infinitely often, then p is true in infinitely many segments of any strictly monotonic function f.
Source project: Lean Computer Science Library
Person-level attribution pending.
cuspForm_rpow_mul_resToImagAxis_tendsto_zero
Mathematical statement
For a cusp form f of level Γ(n), we have t^s * f(it) → 0 as t → ∞ for any real power s. This follows from the exponential decay of cusp forms at infinity: f = O(exp(-2π τ.im / n)).
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
CWSSStructure.toShape_append
Mathematical statement
The shape induced by appended CWSS data is the generic append of the component shapes.
Source project: ArkLib
Person-level attribution pending.
CWSSStructure.toShape_seqCompose
Mathematical statement
The shape induced by finite sequential CWSS data is the generic sequential composition of the component shapes.
Source project: ArkLib
Person-level attribution pending.