Nuprl Lemma : zero-seq_wf

0s ∈ ℕ ⟶ ℕ


Proof




Definitions occuring in Statement :  zero-seq: 0s nat: member: t ∈ T function: x:A ⟶ B[x]
Definitions unfolded in proof :  zero-seq: 0s member: t ∈ T nat: le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A implies:  Q prop: uall: [x:A]. B[x]
Lemmas referenced :  nat_wf le_wf false_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaEquality dependent_set_memberEquality natural_numberEquality independent_pairFormation lambdaFormation hypothesis cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality

Latex:
0s  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}



Date html generated: 2016_05_14-PM-09_54_20
Last ObjectModification: 2016_01_15-AM-06_35_12

Theory : continuity


Home Index