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 31 research declarations. Search 10,000 more complete Mathlib declarations.
31 results
Clear filtersComputablePred.iff_decoded_pred
Plain-language statement
Computability of a predicate on a Primcodable type is equivalent to the computability of the corresponding predicate on ℕ obtained by decoding.
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.Bootstrapping.bv_quote_fixitr
Plain-language statement
bv-pin bridge (over ℕ): bv ⌜fixitr 0 (fvSup χ) ▹ χ⌝ = fvSup χ. - ≤ is immediate from quote_univCl_eq + bv_qqAlls (closing fvSup quantifiers reaches a sentence, whose bv is 0). - ≥ is by level-factoring: were the body an IsSemiformula j for some j < fvSup, IsSemiformula.sound + castLE-invariance would re-express χ as `γ ⇜ ![...
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.Bootstrapping.Derivable.conj
Plain-language statement
Crucial inducion for formalized -completeness.
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.Bootstrapping.fvarVec_val_eq
Plain-language statement
fvarVec is the code of the typed substitution vector fun i ↦ ^&i (over a standard length).
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.of_all
Plain-language statement
Inversion of the bounded-∀ clause: a ^∀-headed 𝚺₁ code is a qqBall.
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.Bootstrapping.le_termBShift
Plain-language statement
termBShift only grows codes: t ≤ termBShift t for well-formed terms. The ^#z → ^#(z+1) bvar shift grows, ^&x is fixed, and functions recurse componentwise. Bounds the ∃ t guard in the bounded-∀ clause.
Source project: Foundation
Person-level attribution pending.