Nuprl Lemma : alist-domain-first
∀[A:Type]
∀d:A List. ∀f1:a:{a:A| (a ∈ d)} ─→ Top. ∀x:A. ∀eq:EqDecider(A).
((x ∈ d)
⇒ (∃i:ℕ||d||. ((∀j:ℕi. (¬((fst(map(λx.<x, f1 x>;d)[j])) = x ∈ A))) ∧ ((fst(map(λx.<x, f1 x>;d)[i])) = x ∈ A))))
Proof
Definitions occuring in Statement :
deq: EqDecider(T)
,
l_member: (x ∈ l)
,
select: L[n]
,
map: map(f;as)
,
length: ||as||
,
list: T List
,
int_seg: {i..j-}
,
uall: ∀[x:A]. B[x]
,
top: Top
,
pi1: fst(t)
,
all: ∀x:A. B[x]
,
exists: ∃x:A. B[x]
,
not: ¬A
,
implies: P
⇒ Q
,
and: P ∧ Q
,
set: {x:A| B[x]}
,
apply: f a
,
lambda: λx.A[x]
,
function: x:A ─→ B[x]
,
pair: <a, b>
,
natural_number: $n
,
universe: Type
,
equal: s = t ∈ T
Lemmas :
l_member-first,
all_wf,
int_seg_wf,
not_wf,
equal_wf,
pi1_wf_top,
select_wf,
map_wf,
sq_stable__le,
map-length,
less_than_transitivity2,
le_weakening2,
l_member_wf,
deq_wf,
top_wf,
list_wf,
select-map,
subtype_rel_list,
length_wf,
lelt_wf
\mforall{}[A:Type]
\mforall{}d:A List. \mforall{}f1:a:\{a:A| (a \mmember{} d)\} {}\mrightarrow{} Top. \mforall{}x:A. \mforall{}eq:EqDecider(A).
((x \mmember{} d)
{}\mRightarrow{} (\mexists{}i:\mBbbN{}||d||
((\mforall{}j:\mBbbN{}i. (\mneg{}((fst(map(\mlambda{}x.<x, f1 x>d)[j])) = x))) \mwedge{} ((fst(map(\mlambda{}x.<x, f1 x>d)[i])) = x))))
Date html generated:
2015_07_17-AM-09_16_32
Last ObjectModification:
2015_01_28-AM-07_53_19
Home
Index