Nuprl Lemma : max-of-intset
∀[P:ℕ ⟶ ℙ]
  ((∀n:ℕ. Dec(P[n]))
  
⇒ (∀n:ℕ. ((∀y:ℕ. ¬P[y] supposing y ≤ n) ∨ (∃y:ℕ. ((y ≤ n) ∧ P[y] ∧ (∀x:ℕ. ¬P[x] supposing y < x ∧ (x ≤ n)))))))
Proof
Definitions occuring in Statement : 
nat: ℕ
, 
less_than: a < b
, 
decidable: Dec(P)
, 
uimplies: b supposing a
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
so_apply: x[s]
, 
le: A ≤ B
, 
all: ∀x:A. B[x]
, 
exists: ∃x:A. B[x]
, 
not: ¬A
, 
implies: P 
⇒ Q
, 
or: P ∨ Q
, 
and: P ∧ Q
, 
function: x:A ⟶ B[x]
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
implies: P 
⇒ Q
, 
all: ∀x:A. B[x]
, 
member: t ∈ T
, 
prop: ℙ
, 
so_lambda: λ2x.t[x]
, 
uimplies: b supposing a
, 
nat: ℕ
, 
so_apply: x[s]
, 
and: P ∧ Q
, 
subtype_rel: A ⊆r B
, 
le: A ≤ B
, 
less_than': less_than'(a;b)
, 
false: False
, 
not: ¬A
, 
decidable: Dec(P)
, 
or: P ∨ Q
, 
guard: {T}
, 
exists: ∃x:A. B[x]
, 
cand: A c∧ B
, 
ge: i ≥ j 
, 
satisfiable_int_formula: satisfiable_int_formula(fmla)
, 
top: Top
, 
sq_type: SQType(T)
Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}]
    ((\mforall{}n:\mBbbN{}.  Dec(P[n]))
    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}
                ((\mforall{}y:\mBbbN{}.  \mneg{}P[y]  supposing  y  \mleq{}  n)
                \mvee{}  (\mexists{}y:\mBbbN{}.  ((y  \mleq{}  n)  \mwedge{}  P[y]  \mwedge{}  (\mforall{}x:\mBbbN{}.  \mneg{}P[x]  supposing  y  <  x  \mwedge{}  (x  \mleq{}  n)))))))
Date html generated:
2016_05_16-AM-10_35_37
Last ObjectModification:
2016_01_17-PM-01_24_22
Theory : new!event-ordering
Home
Index