Nuprl Lemma : fix_wf_corec-family-partial-nat
∀[P:Type]. ∀[H:(P ⟶ Type) ⟶ P ⟶ Type].
∀[f:⋂T:P ⟶ Type. ((i:P ⟶ (T i) ⟶ partial(ℕ)) ⟶ i:P ⟶ (H[T] i) ⟶ partial(ℕ))]
(fix(f) ∈ i:P ⟶ (corec-family(H) i) ⟶ partial(ℕ))
supposing family-monotone{i:l}(P;H) ∧ type-family-continuous{i:l}(P;H)
Proof
Definitions occuring in Statement :
corec-family: corec-family(H),
type-family-continuous: type-family-continuous{i:l}(P;H),
family-monotone: family-monotone{i:l}(P;H),
partial: partial(T),
nat: ℕ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
so_apply: x[s],
and: P ∧ Q,
member: t ∈ T,
apply: f a,
fix: fix(F),
isect: ⋂x:A. B[x],
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
and: P ∧ Q,
nat: ℕ,
so_lambda: λ2x.t[x],
so_apply: x[s],
cand: A c∧ B,
prop: ℙ
Lemmas referenced :
fix_wf_corec-family-partial1,
nat_wf,
set-value-type,
le_wf,
istype-int,
int-value-type,
nat-mono,
partial_wf,
family-monotone_wf,
type-family-continuous_wf,
istype-universe
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
introduction,
cut,
sqequalHypSubstitution,
productElimination,
thin,
extract_by_obid,
isectElimination,
hypothesisEquality,
hypothesis,
independent_isectElimination,
sqequalRule,
intEquality,
Error :lambdaEquality_alt,
natural_numberEquality,
independent_pairFormation,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
Error :isectIsType,
Error :functionIsType,
Error :universeIsType,
Error :inhabitedIsType,
because_Cache,
applyEquality,
Error :isect_memberEquality_alt,
Error :isectIsTypeImplies,
Error :productIsType,
instantiate,
universeEquality
Latex:
\mforall{}[P:Type]. \mforall{}[H:(P {}\mrightarrow{} Type) {}\mrightarrow{} P {}\mrightarrow{} Type].
\mforall{}[f:\mcap{}T:P {}\mrightarrow{} Type. ((i:P {}\mrightarrow{} (T i) {}\mrightarrow{} partial(\mBbbN{})) {}\mrightarrow{} i:P {}\mrightarrow{} (H[T] i) {}\mrightarrow{} partial(\mBbbN{}))]
(fix(f) \mmember{} i:P {}\mrightarrow{} (corec-family(H) i) {}\mrightarrow{} partial(\mBbbN{}))
supposing family-monotone\{i:l\}(P;H) \mwedge{} type-family-continuous\{i:l\}(P;H)
Date html generated:
2019_06_20-PM-00_35_32
Last ObjectModification:
2019_02_20-PM-05_00_56
Theory : co-recursion
Home
Index