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 199 research declarations. Search 10,000 more complete Mathlib declarations.
199 results
Clear filtersCslib.LambdaCalculus.LocallyNameless.Fsub.Typing.weaken
Plain-language statement
Weakening of typings.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.wf
Plain-language statement
Typings have well-formed contexts and types.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LambdaCalculus.LocallyNameless.Stlc.FullBeta.progress
Plain-language 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
Plain-language statement
Closing then opening is equivalent to substitution.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.step_subst_cong_r
Project documentation
Multiple reduction of opening implies multiple reduction of abstraction. -/ theorem redex_abs_cong {M M' : Term Var} (xs : Finset Var) (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠ηᶠ M' ^ fvar x) (lc_M : LC M.abs) : M.abs ↠ηᶠ M'.abs := by cases lc_M case abs L hL => have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var rw [open_close x M 0, open_close x M' 0] all_goals...
Source project: Lean Computer Science Library
Person-level attribution pending.