Nuprl Lemma : null-seq_wf
∀[T:Type]. (null ∈ ℕ0 ─→ T)
Proof
Definitions occuring in Statement :
null-seq: null,
int_seg: {i..j-},
uall: ∀[x:A]. B[x],
member: t ∈ T,
function: x:A ─→ B[x],
natural_number: $n,
universe: Type
Lemmas :
it_wf,
less_than_transitivity1,
less_than_irreflexivity,
int_seg_wf
\mforall{}[T:Type]. (null \mmember{} \mBbbN{}0 {}\mrightarrow{} T)
Date html generated:
2015_07_17-AM-07_58_31
Last ObjectModification:
2015_01_27-AM-11_23_55
Home
Index