AllPredicate
plain-language theorem explainer
Lifts a predicate on values to the pointwise predicate on functions: a display d : I → D satisfies it exactly when every coordinate d(i) satisfies the original predicate. Used wherever completion conservativity is stated for finite function or vector displays. Pure definitional abbreviation; no proof content.
Claim. Given a predicate $P$ on a type $D$, define the pointwise predicate on functions $d : I \to D$ by requiring $P(d(i))$ for every index $i \in I$.
background
In the CompletionConservativity module, a completion is a certificate-bearing extension of a native type, and conservativity means that whenever a completed object satisfies a predicate, some certificate already witnesses that fact on the native side. The basic objects are predicates $P : D \to \mathrm{Prop}$ and completions $C$ of native data $N$ into displays $D$ with certificates.
Finite or display functions $I \to D$ appear as coordinatewise presentations of vectors and fields. To state conservativity for those displays one needs a canonical lift of $P$ from single values to whole functions. That lift is the universal quantification over coordinates: the function is good exactly when every slot is good.
Sibling notions in the same file include product predicates, identity completions, and the conservative-iff-no-artifact characterization; this definition is the function-space counterpart of those pointwise constructions.
proof idea
Definitional one-liner: the body is the lambda fun d => ∀ i : I, P (d i). No lemmas, no tactics, no reduction beyond unfolding.
why it matters
Feeds the two function-space conservativity results in this module. function_conservative states that if a completion $C$ is conservative for $P$, then the function completion is conservative for the pointwise lift; the proof chooses a certificate per index from the pointwise hypothesis. function_completion_headline packages that fact as the headline that certificate-preserving completion is stable under finite function displays, so finite vectors and fields can be certified coordinatewise.
In the broader Recognition foundation this is bookkeeping infrastructure rather than a forcing-chain step: it lets conservativity statements scale from single recognition values to finite displays without inventing new certificate logic. It does not itself invoke T5–T8, the RCL, or the phi ladder; those enter only if the underlying predicate $P$ or completion $C$ already carries them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.