Nuprl Lemma : continuous-monotone-set

[A:Type]. ∀[P:A ⟶ ℙ]. ∀[F:Type ⟶ Type].
  (ContinuousMonotone(T.{x:F[T]| P[x]} )) supposing ((∀T:Type. (F[T] ⊆A)) and ContinuousMonotone(T.F[T]))


Proof




Definitions occuring in Statement :  continuous-monotone: ContinuousMonotone(T.F[T]) uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] set: {x:A| B[x]}  function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  so_apply: x[s] 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] subtype_rel: A ⊆B all: x:A. B[x] implies:  Q prop: type-continuous: Continuous(T.F[T]) guard: {T} nat: le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A squash: T exists: x:A. B[x]
Lemmas referenced :  isect_subtype_rel_trivial set_wf le_wf false_wf continuous-monotone_wf all_wf nat_wf subtype_rel_wf subtype_rel_set subtype_rel_sets
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut independent_pairFormation sqequalHypSubstitution productElimination thin lemma_by_obid isectElimination applyEquality hypothesisEquality lambdaEquality hypothesis dependent_functionElimination independent_isectElimination because_Cache lambdaFormation axiomEquality isect_memberEquality equalityTransitivity equalitySymmetry universeEquality isectEquality setEquality functionEquality cumulativity independent_pairEquality instantiate dependent_set_memberEquality natural_numberEquality setElimination rename imageMemberEquality baseClosed imageElimination dependent_pairFormation

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[F:Type  {}\mrightarrow{}  Type].
    (ContinuousMonotone(T.\{x:F[T]|  P[x]\}  ))  supposing  ((\mforall{}T:Type.  (F[T]  \msubseteq{}r  A))  and  ContinuousMonotone(T\000C.F[T]))



Date html generated: 2016_05_13-PM-04_10_02
Last ObjectModification: 2016_01_14-PM-07_29_48

Theory : subtype_1


Home Index