### Nuprl Lemma : fan_theorem

`∀[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 :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` all: `∀x:A. B[x]` squash: `↓T` implies: `P `` Q` sq_exists: `∃x:A [B[x]]` nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` exists: `∃x:A. B[x]` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` top: `Top` and: `P ∧ Q` prop: `ℙ` int_seg: `{i..j-}` lelt: `i ≤ j < k` so_apply: `x[s1;s2]` le: `A ≤ B` subtype_rel: `A ⊆r B` less_than': `less_than'(a;b)` less_than: `a < b` outl: `outl(x)`
Lemmas referenced :  simple_fan_theorem'-ext set-value-type equal_wf int-value-type nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf intformeq_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_wf istype-le decidable__lt intformless_wf int_formula_prop_less_lemma istype-less_than int_seg_properties int_seg_wf subtype_rel_function nat_wf bool_wf int_seg_subtype_nat istype-false subtype_rel_self istype-nat decidable_wf squash_wf int_seg_decide_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule Error :lambdaEquality_alt,  dependent_functionElimination imageElimination imageMemberEquality baseClosed Error :functionIsTypeImplies,  Error :inhabitedIsType,  rename independent_isectElimination Error :lambdaFormation_alt,  independent_functionElimination setElimination intEquality cutEval Error :dependent_set_memberEquality_alt,  equalityTransitivity equalitySymmetry Error :equalityIstype,  Error :universeIsType,  Error :dependent_pairFormation_alt,  natural_numberEquality unionElimination approximateComputation int_eqEquality Error :isect_memberEquality_alt,  voidElimination independent_pairFormation productElimination Error :productIsType,  because_Cache applyEquality Error :functionIsType,  instantiate universeEquality productEquality functionExtensionality functionEquality

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_29
Last ObjectModification: 2019_01_27-PM-01_53_25

Theory : int_2

Home Index