Nuprl Lemma : compact-union

[T,S:Type].  (compact-type(T)  compact-type(S)  compact-type(T S))


Proof




Definitions occuring in Statement :  compact-type: compact-type(T) uall: [x:A]. B[x] implies:  Q union: left right universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] implies:  Q compact-type: compact-type(T) all: x:A. B[x] member: t ∈ T prop: or: P ∨ Q exists: x:A. B[x] so_lambda: λ2x.t[x] so_apply: x[s] guard: {T} squash: T true: True subtype_rel: A ⊆B uimplies: supposing a iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q
Lemmas referenced :  bool_wf compact-type_wf equal-wf-T-base all_wf equal_wf squash_wf true_wf btrue_wf iff_weakening_equal exists_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalHypSubstitution functionEquality unionEquality cumulativity hypothesisEquality cut introduction extract_by_obid hypothesis isectElimination thin universeEquality dependent_functionElimination lambdaEquality applyEquality functionExtensionality inlEquality sqequalRule unionElimination productElimination inlFormation dependent_pairFormation baseClosed inrEquality inrFormation imageElimination equalityTransitivity equalitySymmetry natural_numberEquality imageMemberEquality independent_isectElimination independent_functionElimination because_Cache

Latex:
\mforall{}[T,S:Type].    (compact-type(T)  {}\mRightarrow{}  compact-type(S)  {}\mRightarrow{}  compact-type(T  +  S))



Date html generated: 2017_10_01-AM-08_29_00
Last ObjectModification: 2017_07_26-PM-04_23_46

Theory : basic


Home Index