### Nuprl Lemma : urec-is-fixedpoint

`∀[F:Type ⟶ Type]. F urec(F) ≡ urec(F) supposing continuous'-monotone{i:l}(T.F T)`

Proof

Definitions occuring in Statement :  continuous'-monotone: `continuous'-monotone{i:l}(T.F[T])` urec: `urec(F)` ext-eq: `A ≡ B` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` ext-eq: `A ≡ B` and: `P ∧ Q` continuous'-monotone: `continuous'-monotone{i:l}(T.F[T])` so_apply: `x[s]` subtype_rel: `A ⊆r B` prop: `ℙ` so_lambda: `λ2x.t[x]`
Lemmas referenced :  subtype_urec urec_subtype continuous'-monotone_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination hypothesis productElimination sqequalRule independent_pairEquality axiomEquality lambdaEquality applyEquality universeEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry functionEquality

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type].  F  urec(F)  \mequiv{}  urec(F)  supposing  continuous'-monotone\{i:l\}(T.F  T)

Date html generated: 2016_05_15-PM-06_54_38
Last ObjectModification: 2015_12_27-AM-11_41_23

Theory : general

Home Index