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