### 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