PD0001

Le(a,b)

Witness-defined non-strict order on natural numbers.

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

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

a ≤ b

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

Hygienic expanded first-order definition 
exists h. h + a = b

The 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

ArithPositiveEqual(F,G,N)SignedZeroWindow(F,k,l)ArithTable(N,F)DirichletPrefix(F,G,n,l,M)DirichletTable(N,F,G,H)

Checked theorems using this definition

DC0009 · dirichlet_convolution_prefix_appendDC000B · dirichlet_convolution_prefix_lookupDC000C · dirichlet_convolution_prefix_extensionalDC000D · dirichlet_convolution_prefix_restrictDC000E · dirichlet_convolution_prefix_quotient_entryDC000F · dirichlet_convolution_prefix_omitted_entryDC0010 · dirichlet_convolution_sum_existsDC0012 · dirichlet_convolution_sum_exists_uniqueDC0014 · dirichlet_convolution_entry_positive_source_extensionalDC0015 · dirichlet_convolution_prefix_positive_source_extensionalDC0017 · dirichlet_convolution_positive_source_transportDC0019 · dirichlet_convolution_table_appendDC001B · dirichlet_convolution_table_lookupDC001E · dirichlet_convolution_table_restrictDC0020 · dirichlet_convolution_prefix_value_from_entryDC0021 · dirichlet_convolution_prefix_complement_reindexDC0023 · dirichlet_convolution_sum_swapDC0027 · dirichlet_convolution_from_padded_prefixDC0028 · dirichlet_convolution_padded_prefix_iff