Nuprl Lemma : awf-solution_wf
∀[A,I:Type].
∀G:awf-system{i:l}(I;A)
(awf-solution(G) ∈ {s:I ⟶ awf(A)|
(∀i:I. ((s i) = (G s i) ∈ awf(A)))
∧ (∀s':I ⟶ awf(A). ((∀i:I. ((s' i) = (G s' i) ∈ awf(A))) ⇒ (s' = s ∈ (I ⟶ awf(A)))))} )
Proof
Definitions occuring in Statement :
awf-solution: awf-solution(G),
awf-system: awf-system{i:l}(I;A),
awf: awf(T),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
member: t ∈ T,
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
unique-corec-solution,
corec-ext,
unique-awf,
awf-solution: awf-solution(G),
sq_exists: ∃x:A [B[x]],
subtype_rel: A ⊆r B,
implies: P ⇒ Q,
and: P ∧ Q
Lemmas referenced :
awf-system_wf,
unique-awf,
awf_wf,
awf-system-subtype,
unique-corec-solution,
corec-ext
Rules used in proof :
universeEquality,
hypothesisEquality,
cumulativity,
thin,
isectElimination,
extract_by_obid,
introduction,
hypothesis,
sqequalHypSubstitution,
cut,
lambdaFormation,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
sqequalRule,
applyEquality,
instantiate,
lambdaEquality_alt,
equalityTransitivity,
equalitySymmetry,
inhabitedIsType,
lambdaFormation_alt,
equalityIstype,
dependent_functionElimination,
independent_functionElimination,
isectIsType,
because_Cache,
functionIsType,
universeIsType,
setIsType,
productIsType
Latex:
\mforall{}[A,I:Type].
\mforall{}G:awf-system\{i:l\}(I;A)
(awf-solution(G) \mmember{} \{s:I {}\mrightarrow{} awf(A)|
(\mforall{}i:I. ((s i) = (G s i)))
\mwedge{} (\mforall{}s':I {}\mrightarrow{} awf(A). ((\mforall{}i:I. ((s' i) = (G s' i))) {}\mRightarrow{} (s' = s)))\} )
Date html generated:
2020_05_20-AM-08_19_50
Last ObjectModification:
2020_01_08-AM-11_23_50
Theory : general
Home
Index