Nuprl Lemma : ext2Baire_wf

[n:ℕ]. ∀[f:ℕn ⟶ ℕ]. ∀[d:ℕ].  (ext2Baire(n;f;d) ∈ ℕ ⟶ ℕ)


Proof




Definitions occuring in Statement :  ext2Baire: ext2Baire(n;f;d) int_seg: {i..j-} nat: uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T ext2Baire: ext2Baire(n;f;d) nat: all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a int_seg: {i..j-} lelt: i ≤ j < k le: A ≤ B prop: bfalse: ff
Lemmas referenced :  lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int int_seg_wf lelt_wf equal_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lambdaEquality extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename because_Cache hypothesis lambdaFormation unionElimination equalityElimination productElimination independent_isectElimination applyEquality functionExtensionality hypothesisEquality natural_numberEquality dependent_set_memberEquality independent_pairFormation equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination axiomEquality isect_memberEquality functionEquality

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[d:\mBbbN{}].    (ext2Baire(n;f;d)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{})



Date html generated: 2017_04_17-AM-09_59_47
Last ObjectModification: 2017_02_27-PM-05_52_21

Theory : continuity


Home Index