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 136 research declarations. Search 10,000 more complete Mathlib declarations.
136 results
Clear filtersCslib.LambdaCalculus.LocallyNameless.Untyped.Term.sn_abs_app_multiApp
Plain-language statement
A term of the form λ M N P_1 … P_n is strongly normalizing if 1. N is strongly normalizing, 1. M ^ N P₁ … Pₙ is strongly normalizing, 1. N is locally closed, 1. M ^ N P₁ … Pₙ is locally closed
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.sn_app
Plain-language statement
An application is strongly normalizing if the left and right terms are strongly normalizing, as well as all possible future top level abstraction application beta reductions
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.abs_inv
Plain-language statement
If a standard reduction reaches an abstraction, then its leading Call-by-Name reduction reaches an abstraction that standardly reduces to the same target.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.subst
Plain-language statement
Standard reduction is preserved by substitution.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.to_redex
Plain-language statement
Standard reduction is contained in full β-reduction.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.trans_step
Plain-language statement
A standard reduction followed by a full β-step is a standard reduction.
Source project: Lean Computer Science Library
Person-level attribution pending.