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 619 to 624 of 2,569 results.
Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.tabs_inv
Mathematical statement
Invert the typing of a type abstraction.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.weaken
Mathematical statement
Weakening of typings.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.wf
Mathematical statement
Typings have well-formed contexts and types.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LambdaCalculus.LocallyNameless.Stlc.FullBeta.progress
Mathematical statement
A typed term either full beta reduces or is a value.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LambdaCalculus.LocallyNameless.Stlc.soundness
Project documentation
The soundness lemma states that if a term t has type τ in context Γ, then t is semantically valid with respect to Γ and τ
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.close_openRec_to_subst
Mathematical statement
Closing then opening is equivalent to substitution.
Source project: Lean Computer Science Library
Person-level attribution pending.