Nuprl Definition : uwellfounded
uWellFnd(A;x,y.R[x; y]) == ∀[P:A ⟶ ℙ]. ((∀[j:A]. ((∀[k:{k:A| R[k; j]} ]. P[k]) ⇒ P[j])) ⇒ (∀[n:A]. P[n]))
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x]
Definitions occuring in definition :
function: x:A ⟶ B[x],
prop: ℙ,
implies: P ⇒ Q,
set: {x:A| B[x]} ,
uall: ∀[x:A]. B[x],
so_apply: x[s]
FDL editor aliases :
pwellfounded
Latex:
uWellFnd(A;x,y.R[x; y]) ==
\mforall{}[P:A {}\mrightarrow{} \mBbbP{}]. ((\mforall{}[j:A]. ((\mforall{}[k:\{k:A| R[k; j]\} ]. P[k]) {}\mRightarrow{} P[j])) {}\mRightarrow{} (\mforall{}[n:A]. P[n]))
Date html generated:
2016_05_13-PM-03_18_12
Last ObjectModification:
2016_01_04-AM-10_27_04
Theory : well_fnd
Home
Index