Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Definition in prerequisite notation
S a ≤ bOnly definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists h. h + S a = bThe unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
none — first-order arithmetic only
Definitions depending on this notation
DivRem(n,d,q,r)ArithTableEqual(F,G,l)ArithScale(a,F,G,l)Sum(b,c,l,z)ArithSlice(F,G,o,s,l)ArithRowSums(F,R,o,s,t,m,n)SignedZeroWindow(F,k,l)DivisorPairIndexMap(V,L,r,s)SignedCartesianProduct(F,G,T,m,n)SignedSupportReindex(A,B,r,s,L,M)SignedIncidenceFlatEntry(A,r,s,M,k,z)SignedSupportIncidence(A,r,s,L,M,T)DirichletDivisorGridWitness(F,G,m,n,i,z,d,e,a,b)
Checked theorems using this definition
MX0014 · divisor_pair_index_map_appendMX0015 · divisor_pair_index_map_existsMX0016 · divisor_pair_index_map_lookupMX0017 · divisor_pair_index_map_valueMX001F · signed_cartesian_flat_entry_existsMX0020 · signed_cartesian_flat_entry_lookupMX0021 · signed_cartesian_flat_prefix_zeroMX0022 · signed_cartesian_flat_prefix_appendMX0023 · signed_cartesian_flat_prefix_existsMX0024 · signed_cartesian_product_from_flat_prefixMX0026 · signed_cartesian_product_existsMX0027 · signed_cartesian_product_row_scalarMX0028 · signed_cartesian_product_row_sumMX002D · signed_cartesian_quotient_row_boundMX002E · signed_cartesian_coordinates_existsMX002F · signed_cartesian_product_flat_lookupMX0030 · signed_cartesian_product_extensional_uniqueMX0033 · signed_prefix_sum_single_spike_valueMX0034 · signed_prefix_sum_single_spike_existsMX0035 · signed_prefix_sum_point_spike_valueMX003E · signed_support_incidence_flat_entry_coordinatesMX0040 · signed_support_incidence_flat_prefix_appendMX0044 · signed_support_incidence_row_lookupMX0045 · signed_support_incidence_column_lookupMX0046 · signed_support_incidence_row_sum_valueMX0047 · signed_support_incidence_column_sum_valueMX0051 · dirichlet_coprime_grid_nonzero_coordinatesMX0052 · dirichlet_coprime_grid_support_preservingMX0053 · dirichlet_coprime_grid_support_injectiveMX0054 · dirichlet_coprime_grid_support_covering