Nuprl Lemma : mData-examples
(<ℤ, 33> ∈ mData) ∧ (<𝔹, tt> ∈ mData) ∧ (<ℤ ─→ ℤ, λx.(x + 1)> ∈ mData) ∧ (<ℤ × 𝔹, 33, ff> ∈ mData)
Proof
Definitions occuring in Statement :
mData: mData,
bfalse: ff,
btrue: tt,
bool: 𝔹,
and: P ∧ Q,
member: t ∈ T,
lambda: λx.A[x],
function: x:A ─→ B[x],
pair: <a, b>,
product: x:A × B[x],
add: n + m,
natural_number: $n,
int: ℤ
Lemmas :
subtype_rel_self,
base_wf,
subtype_base_sq,
bool_wf,
bfalse_wf,
subtype_rel_product,
subtype_rel-equal,
mData_wf,
btrue_wf
Latex:
(<\mBbbZ{}, 33> \mmember{} mData) \mwedge{} (<\mBbbB{}, tt> \mmember{} mData) \mwedge{} (<\mBbbZ{} {}\mrightarrow{} \mBbbZ{}, \mlambda{}x.(x + 1)> \mmember{} mData) \mwedge{} (<\mBbbZ{} \mtimes{} \mBbbB{}, 33, ff> \mmember{} mData)
Date html generated:
2015_07_21-PM-04_48_01
Last ObjectModification:
2015_01_28-AM-08_47_03
Home
Index