Nuprl Lemma : per-all_wf
∀[A:Type]. ∀[B:type-function{i:l}(A)]. (per-all(A;a.B[a]) ∈ ℙ)
Proof
Definitions occuring in Statement :
per-all: per-all(A;a.B[a]),
type-function: type-function{i:l}(A),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
member: t ∈ T,
universe: Type
Definitions unfolded in proof :
per-all: per-all(A;a.B[a]),
so_apply: x[s],
prop: ℙ,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
per-function_wf
Rules used in proof :
cut,
lemma_by_obid,
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
sqequalHypSubstitution,
hypothesis
Latex:
\mforall{}[A:Type]. \mforall{}[B:type-function\{i:l\}(A)]. (per-all(A;a.B[a]) \mmember{} \mBbbP{})
Date html generated:
2016_05_13-PM-03_54_11
Last ObjectModification:
2015_12_26-AM-10_40_49
Theory : per!type
Home
Index