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: ℤ
Definitions unfolded in proof :
and: P ∧ Q,
cand: A c∧ B,
mData: mData,
member: t ∈ T
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:
2016_05_17-AM-08_49_45
Last ObjectModification:
2015_12_29-PM-02_57_39
Theory : messages
Home
Index