Nuprl Lemma : init0-cantor2baire

`∀a:ℕ ⟶ 𝔹. init0(cantor2baire(a))`

Proof

Definitions occuring in Statement :  init0: `init0(a)` cantor2baire: `cantor2baire(a)` nat: `ℕ` bool: `𝔹` all: `∀x:A. B[x]` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  implies: `P `` Q` not: `¬A` less_than': `less_than'(a;b)` and: `P ∧ Q` le: `A ≤ B` nat: `ℕ` false: `False` prop: `ℙ` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` or: `P ∨ Q` decidable: `Dec(P)` top: `Top` member: `t ∈ T` cantor2baire-aux: `cantor2baire-aux(a;n)` init0: `init0(a)` cantor2baire: `cantor2baire(a)` all: `∀x:A. B[x]`
Lemmas referenced :  bool_wf nat_wf le_wf false_wf int_formula_prop_wf int_term_value_constant_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma itermConstant_wf intformeq_wf intformnot_wf satisfiable-full-omega-tt decidable__equal_int primrec0_lemma
Rules used in proof :  functionEquality independent_pairFormation equalitySymmetry equalityTransitivity dependent_set_memberEquality computeAll hypothesisEquality intEquality lambdaEquality dependent_pairFormation independent_isectElimination isectElimination unionElimination because_Cache natural_numberEquality hypothesis voidEquality voidElimination isect_memberEquality thin dependent_functionElimination sqequalHypSubstitution extract_by_obid introduction cut sqequalRule lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  init0(cantor2baire(a))

Date html generated: 2017_04_21-AM-11_22_27
Last ObjectModification: 2017_04_20-PM-04_24_21

Theory : continuity

Home Index