pr1 \(\mathrm{pr}_1\) — First Class-Pair Projection Functional Symbol (pr1, Entry DefDunaevOrderedPair (3.76))
Unary functional symbol pr1(L) = {a | ({{{a}}, 1} ∈ L)} extracting the first component of a Dunaev class-pair (Entries DefDunaevOrderedPair (3.76), RulClassComprehension (3.01)).
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
pr1
\(\mathrm{pr}_1\)
|
| Category | Functional Symbol (Unary Class Operator) |
| SML AST Constructor | Pr1_def_entry [Defined Unary Functional Symbol, entries.ML:DefDunaevOrderedPair (3.76)] |
| Constructor Arguments | 1. Dunaev class-pair L : Class |
| Metatype / Signature | Class → Class |
| Binder Status | No — Unary Functional Symbol (First Class-Pair Projection) |
| Defining Kernel Entries (ML Labels) | See Related Symbols & Kernel Entries below. |
| LaTeX Form | \mathrm{pr}_1 |
| How to Understand It | SML AST Constructor: Defined unary class operator in Entry DefDunaevOrderedPair (3.76) ( |
| Canonical Law / Usage | pr1((A, B)) = A |
| Related Symbols & Kernel Entries |