Nuprl Lemma : FAN_wf
∀[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
∀[d:∀n:ℕ. ∀s:ℕn ⟶ 𝔹. Dec(X[n;s])]. (FAN(d) ∈ {k:ℕ| ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f]} ) supposing ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. X[n;f])
Proof
Definitions occuring in Statement :
FAN: FAN(d),
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,
member: t ∈ T,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
natural_number: $n
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
sq_exists: ∃x:A [B[x]],
FAN: FAN(d),
bar_recursion: bar_recursion,
simple_fan_theorem'-ext,
member: t ∈ T,
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
so_apply: x[s1;s2],
exists: ∃x:A. B[x],
prop: ℙ,
nat: ℕ,
le: A ≤ B,
and: P ∧ Q,
less_than': less_than'(a;b),
false: False,
not: ¬A,
int_seg: {i..j-},
lelt: i ≤ j < k
Lemmas referenced :
simple_fan_theorem'-ext,
istype-nat,
bool_wf,
squash_wf,
nat_wf,
int_seg_wf,
decidable_wf,
int_seg_subtype_nat,
istype-false,
subtype_rel_function,
subtype_rel_self
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
sqequalRule,
applyEquality,
cut,
thin,
instantiate,
extract_by_obid,
hypothesis,
Error :lambdaEquality_alt,
isectElimination,
hypothesisEquality,
equalityTransitivity,
equalitySymmetry,
Error :inhabitedIsType,
Error :lambdaFormation_alt,
sqequalHypSubstitution,
rename,
Error :equalityIstype,
dependent_functionElimination,
independent_functionElimination,
Error :isectIsType,
Error :functionIsType,
introduction,
Error :universeIsType,
productEquality,
because_Cache,
natural_numberEquality,
setElimination,
Error :setIsType,
Error :productIsType,
independent_isectElimination,
independent_pairFormation,
productElimination,
universeEquality
Latex:
\mforall{}[X:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} \mBbbB{}) {}\mrightarrow{} \mBbbP{}]
\mforall{}[d:\mforall{}n:\mBbbN{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} \mBbbB{}. Dec(X[n;s])]. (FAN(d) \mmember{} \{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-AM-11_33_05
Last ObjectModification:
2019_01_27-PM-01_40_00
Theory : bool_1
Home
Index