Nuprl Lemma : continuous'-monotone-sum

[F,G:Type ⟶ Type].
  (continuous'-monotone{i:l}(T.F[T] G[T])) supposing 
     (continuous'-monotone{i:l}(T.G[T]) and 
     continuous'-monotone{i:l}(T.F[T]))


Proof




Definitions occuring in Statement :  continuous'-monotone: continuous'-monotone{i:l}(T.F[T]) uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] function: x:A ⟶ B[x] union: left right universe: Type
Definitions unfolded in proof :  so_apply: x[s] continuous'-monotone: continuous'-monotone{i:l}(T.F[T]) uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a and: P ∧ Q cand: c∧ B type-monotone: Monotone(T.F[T]) subtype_rel: A ⊆B type-continuous': semi-continuous(λT.F[T]) so_lambda: λ2x.t[x] type-incr-chain: type-incr-chain{i:l}() tunion: x:A.B[x] pi2: snd(t) prop:
Lemmas referenced :  type-continuous'_wf type-monotone_wf and_wf type-incr-chain_wf nat_wf tunion_wf subtype_rel_union subtype_rel_wf subtype_rel_sum
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin lemma_by_obid isectElimination applyEquality hypothesisEquality independent_isectElimination hypothesis axiomEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry universeEquality independent_pairFormation lambdaEquality setElimination rename unionElimination imageElimination imageMemberEquality dependent_pairEquality inlEquality unionEquality baseClosed inrEquality independent_pairEquality instantiate functionEquality

Latex:
\mforall{}[F,G:Type  {}\mrightarrow{}  Type].
    (continuous'-monotone\{i:l\}(T.F[T]  +  G[T]))  supposing 
          (continuous'-monotone\{i:l\}(T.G[T])  and 
          continuous'-monotone\{i:l\}(T.F[T]))



Date html generated: 2016_05_15-PM-06_53_25
Last ObjectModification: 2016_01_16-AM-09_49_02

Theory : general


Home Index