### Nuprl Lemma : rel-monotone_wf

`∀[T:Type]. ∀[F:(T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ].  (rel-monotone{i:l}(T;R.F[R]) ∈ ℙ')`

Proof

Definitions occuring in Statement :  rel-monotone: `rel-monotone{i:l}(T;R.F[R])` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` rel-monotone: `rel-monotone{i:l}(T;R.F[R])` prop: `ℙ` so_lambda: `λ2x.t[x]` implies: `P `` Q` so_apply: `x[s]`
Lemmas referenced :  all_wf rel_implies_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule thin instantiate lemma_by_obid sqequalHypSubstitution isectElimination functionEquality cumulativity hypothesisEquality universeEquality lambdaEquality hypothesis applyEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[T:Type].  \mforall{}[F:(T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (rel-monotone\{i:l\}(T;R.F[R])  \mmember{}  \mBbbP{}')

Date html generated: 2016_05_14-AM-06_04_56
Last ObjectModification: 2015_12_26-AM-11_33_01

Theory : relations

Home Index