Nuprl Lemma : type-monotone-union-continuous

[F:Type ⟶ Type]. union-continuous{i:l}(T.F[T]) supposing Monotone(T.F[T])


Proof




Definitions occuring in Statement :  union-continuous: union-continuous{i:l}(T.F[T]) type-monotone: Monotone(T.F[T]) uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a union-continuous: union-continuous{i:l}(T.F[T]) subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] prop: tunion: x:A.B[x] pi2: snd(t) type-monotone: Monotone(T.F[T])
Lemmas referenced :  type-monotone_wf tunion_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule applyEquality hypothesis axiomEquality functionEquality cumulativity universeEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry imageElimination productElimination independent_isectElimination imageMemberEquality dependent_pairEquality baseClosed

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type].  union-continuous\{i:l\}(T.F[T])  supposing  Monotone(T.F[T])



Date html generated: 2016_05_13-PM-04_10_20
Last ObjectModification: 2016_01_14-PM-07_29_47

Theory : subtype_1


Home Index