Nuprl Lemma : strong-continuity3_wf

[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ].  (strong-continuity3(T;F) ∈ ℙ)


Proof




Definitions occuring in Statement :  strong-continuity3: strong-continuity3(T;F) nat: uall: [x:A]. B[x] prop: member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T strong-continuity3: strong-continuity3(T;F) nat: so_lambda: λ2x.t[x] prop: and: P ∧ Q subtype_rel: A ⊆B so_apply: x[s] uimplies: supposing a le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A implies:  Q all: x:A. B[x]
Lemmas referenced :  exists_wf nat_wf int_seg_wf unit_wf2 all_wf equal_wf subtype_rel_dep_function int_seg_subtype_nat false_wf assert_wf isl_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin functionEquality hypothesis natural_numberEquality setElimination rename because_Cache cumulativity hypothesisEquality unionEquality lambdaEquality productEquality applyEquality functionExtensionality independent_isectElimination independent_pairFormation lambdaFormation inlEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}].    (strong-continuity3(T;F)  \mmember{}  \mBbbP{})



Date html generated: 2017_04_17-AM-09_53_43
Last ObjectModification: 2017_02_27-PM-05_48_40

Theory : continuity


Home Index