Nuprl Lemma : sequence_subtype

[A,B:Type].  sequence(A) ⊆sequence(B) supposing A ⊆B


Proof




Definitions occuring in Statement :  sequence: sequence(T) uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  all: x:A. B[x] subtype_rel: A ⊆B so_apply: x[s] nat: so_lambda: λ2x.t[x] uimplies: supposing a member: t ∈ T uall: [x:A]. B[x] sequence: sequence(T)
Lemmas referenced :  subtype_rel_wf subtype_rel_dep_function int_seg_wf nat_wf subtype_rel_product
Rules used in proof :  universeEquality equalitySymmetry equalityTransitivity isect_memberEquality axiomEquality lambdaFormation independent_isectElimination because_Cache hypothesisEquality rename setElimination natural_numberEquality functionEquality lambdaEquality hypothesis thin isectElimination sqequalHypSubstitution extract_by_obid cut introduction isect_memberFormation computationStep sqequalTransitivity sqequalReflexivity sqequalRule sqequalSubstitution

Latex:
\mforall{}[A,B:Type].    sequence(A)  \msubseteq{}r  sequence(B)  supposing  A  \msubseteq{}r  B



Date html generated: 2018_07_25-PM-01_29_34
Last ObjectModification: 2018_06_18-PM-10_51_19

Theory : arithmetic


Home Index