PD0026

SurjectivePrefix(b,c,l)

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

Every value below l occurs at an index below l.

Conservative notation; not a theorem, primitive, or axiom.

Definition in prerequisite notation

∀ fp_value_defined_surjective_prefix. Lt(fp_value_defined_surjective_prefix,l) → ∃ x. Lt(x,l) ∧ BetaAt(b,c,x,fp_value_defined_surjective_prefix)

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition 
forall fp_value_defined_surjective_prefix. (exists fp_gap_defined_surjective_prefix_value. fp_gap_defined_surjective_prefix_value + S fp_value_defined_surjective_prefix = l) -> exists fp_i_defined_surjective_prefix. ((exists fp_gap_defined_surjective_prefix_index. fp_gap_defined_surjective_prefix_index + S fp_i_defined_surjective_prefix = l) /\ (((exists ff_h_defined_surjective_prefix_entry. ff_h_defined_surjective_prefix_entry + S (fp_value_defined_surjective_prefix) = S ((S (fp_i_defined_surjective_prefix)) * c)) /\ exists ff_q_defined_surjective_prefix_entry. b = ff_q_defined_surjective_prefix_entry * S ((S (fp_i_defined_surjective_prefix)) * c) + (fp_value_defined_surjective_prefix))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

Lt(a,b)BetaAt(b,c,i,x)

Definitions depending on this notation

PermutationPrefix(b,c,l)

Checked theorems using this definition

none directly; see definition consumers