Nuprl Lemma : fan_theorem-ext
∀[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
  (∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s])) 
⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f]) supposing ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. X[n;f])
Proof
Definitions occuring in Statement : 
int_seg: {i..j-}
, 
nat: ℕ
, 
bool: 𝔹
, 
decidable: Dec(P)
, 
uimplies: b supposing a
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
so_apply: x[s1;s2]
, 
all: ∀x:A. B[x]
, 
exists: ∃x:A. B[x]
, 
squash: ↓T
, 
implies: P 
⇒ Q
, 
function: x:A ⟶ B[x]
, 
natural_number: $n
Definitions unfolded in proof : 
member: t ∈ T
, 
fan_theorem, 
simple_fan_theorem'-ext
Lemmas referenced : 
fan_theorem, 
simple_fan_theorem'-ext
Rules used in proof : 
introduction, 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
cut, 
instantiate, 
extract_by_obid, 
hypothesis, 
sqequalRule, 
thin, 
sqequalHypSubstitution, 
equalityTransitivity, 
equalitySymmetry
Latex:
\mforall{}[X:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbP{}]
    (\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.    Dec(X[n;s]))  {}\mRightarrow{}  (\mexists{}k:\mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}k.  X[n;f]) 
    supposing  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (\mdownarrow{}\mexists{}n:\mBbbN{}.  X[n;f])
Date html generated:
2019_06_20-PM-01_15_32
Last ObjectModification:
2019_03_12-PM-04_25_58
Theory : int_2
Home
Index