Nuprl Lemma : Kleene-M_wf
∀[T:{T:Type| (T ⊆r ℕ) ∧ (↓T)} ]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. (Kleene-M(F) ∈ ⇃(basic-strong-continuity(T;F)))
Proof
Definitions occuring in Statement :
Kleene-M: Kleene-M(F),
basic-strong-continuity: basic-strong-continuity(T;F),
quotient: x,y:A//B[x; y],
nat: ℕ,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
squash: ↓T,
and: P ∧ Q,
true: True,
member: t ∈ T,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
and: P ∧ Q,
squash: ↓T,
sq_stable: SqStable(P),
implies: P ⇒ Q,
bound-domain: bound-domain(f;n;e),
Kleene-M: Kleene-M(F),
sq_exists: ∃x:A [B[x]],
basic-strong-continuity: basic-strong-continuity(T;F),
prop: ℙ
Lemmas referenced :
sq_stable__subtype_rel,
nat_wf,
istype-nat,
istype-universe,
subtype_rel_wf,
squash_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
introduction,
cut,
StrongContinuity2,
hypothesisEquality,
setElimination,
thin,
rename,
sqequalHypSubstitution,
productElimination,
hypothesis,
imageElimination,
sqequalRule,
imageMemberEquality,
baseClosed,
extract_by_obid,
isectElimination,
independent_functionElimination,
equalityTransitivity,
equalitySymmetry,
axiomEquality,
Error :functionIsType,
Error :universeIsType,
because_Cache,
Error :isect_memberEquality_alt,
Error :isectIsTypeImplies,
Error :inhabitedIsType,
Error :setIsType,
instantiate,
universeEquality,
Error :productIsType
Latex:
\mforall{}[T:\{T:Type| (T \msubseteq{}r \mBbbN{}) \mwedge{} (\mdownarrow{}T)\} ]. \mforall{}[F:(\mBbbN{} {}\mrightarrow{} T) {}\mrightarrow{} \mBbbN{}].
(Kleene-M(F) \mmember{} \00D9(basic-strong-continuity(T;F)))
Date html generated:
2019_06_20-PM-02_50_46
Last ObjectModification:
2019_02_11-AM-11_19_59
Theory : continuity
Home
Index