Nuprl Definition : nat-prop
nat-prop{i:l}(n) == if (n) < (1) then Top else P:nat-prop{i:l}(n - 1) ⋂ j:ℕn ⟶ ℙ supposing dep-all(j;i.P i)
Definitions occuring in Statement :
dep-isect: x:A ⋂ B[x],
int_seg: {i..j-},
uimplies: b supposing a,
top: Top,
prop: ℙ,
less: if (a) < (b) then c else d,
apply: f a,
function: x:A ⟶ B[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
less: if (a) < (b) then c else d,
top: Top,
dep-isect: x:A ⋂ B[x],
subtract: n - m,
function: x:A ⟶ B[x],
int_seg: {i..j-},
natural_number: $n,
uimplies: b supposing a,
apply: f a,
prop: ℙ
FDL editor aliases :
nat-prop
Latex:
nat-prop\{i:l\}(n) ==
if (n) < (1) then Top else P:nat-prop\{i:l\}(n - 1) \mcap{} j:\mBbbN{}n {}\mrightarrow{} \mBbbP{} supposing dep-all(j;i.P i)
Date html generated:
2020_05_19-PM-09_39_42
Last ObjectModification:
2020_03_04-PM-03_06_58
Theory : co-recursion-2
Home
Index