### Nuprl Lemma : sequence_subtype

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

Proof

Definitions occuring in Statement :  sequence: `sequence(T)` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` subtype_rel: `A ⊆r B` so_apply: `x[s]` nat: `ℕ` so_lambda: `λ2x.t[x]` uimplies: `b 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