Nuprl Lemma : continuous-monotone-isect

[A:Type]. ∀[F:A ⟶ Type ⟶ Type].  ContinuousMonotone(T.⋂a:A. F[a;T]) supposing ∀a:A. ContinuousMonotone(T.F[a;T])


Proof




Definitions occuring in Statement :  continuous-monotone: ContinuousMonotone(T.F[T]) uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s1;s2] all: x:A. B[x] isect: x:A. B[x] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  so_apply: x[s1;s2] uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a continuous-monotone: ContinuousMonotone(T.F[T]) and: P ∧ Q type-monotone: Monotone(T.F[T]) so_lambda: λ2x.t[x] so_apply: x[s] uiff: uiff(P;Q) subtype_rel: A ⊆B all: x:A. B[x] implies:  Q type-continuous: Continuous(T.F[T]) prop: strong-type-continuous: Continuous+(T.F[T]) ext-eq: A ≡ B guard: {T}
Lemmas referenced :  subtype_rel_isect equal_wf subtype_rel_wf nat_wf subtype_rel_weakening all_wf continuous-monotone_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut independent_pairFormation extract_by_obid sqequalHypSubstitution isectElimination thin isectEquality cumulativity hypothesisEquality applyEquality functionExtensionality lambdaEquality productElimination independent_isectElimination equalityTransitivity equalitySymmetry hypothesis lambdaFormation dependent_functionElimination independent_functionElimination because_Cache axiomEquality isect_memberEquality universeEquality independent_pairEquality functionEquality instantiate

Latex:
\mforall{}[A:Type].  \mforall{}[F:A  {}\mrightarrow{}  Type  {}\mrightarrow{}  Type].
    ContinuousMonotone(T.\mcap{}a:A.  F[a;T])  supposing  \mforall{}a:A.  ContinuousMonotone(T.F[a;T])



Date html generated: 2017_04_14-AM-07_36_34
Last ObjectModification: 2017_02_27-PM-03_08_46

Theory : subtype_1


Home Index