∩ \(\cap\) — Binary Class Intersection Functional Symbol (∩, AST Constructor: CpBinInter)
Binary class intersection functional symbol A ∩ B = {x | (x∈A) ∧ (x∈B)} (Entry DefBinaryIntersection (3.54)).
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
∩
\(\cap\)
|
| Category | Functional Symbol (Binary Class Operator) |
| SML AST Constructor | HC (CpBinInter of ('Class_EXP * 'Class_EXP)) [in datatype Class_p, typetheory.ML:567] |
| Constructor Arguments | 1. Left class A : Class; 2. Right class B : Class |
| Metatype / Signature | Class × Class → Class |
| Binder Status | No — Binary Functional Symbol (Binary Intersection) |
| Defining Kernel Entries (ML Labels) | Definition DefBinaryIntersection (3.54): Binary intersection (#DefBinaryIntersection / #label-binary-intersection) |
| LaTeX Form | \cap |
| How to Understand It | SML AST Constructor: |
| Canonical Law / Usage | ∀(A:Class)∀(B:Class)((A ∩ B) = {x | (x ∈ A) ∧ (x ∈ B)}) |
| Related Symbols & Kernel Entries |
Defining Axioms, Rules & Formal Definitions (Rendered Directly from Kernel Entries)
Generated without code duplication by invoking render_entry_row_base "../manual.html" on the corresponding kernel Entry records.
| # | Formal Entity Specification | ||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 3.54 |
|