Nuprl Definition : indNat
INat == x:cNat ⋂ church-inductive{i:l}(x)
Definitions occuring in Statement :
church-inductive: church-inductive{i:l}(x),
church-Nat: cNat,
dep-isect: x:A ⋂ B[x]
Definitions occuring in definition :
dep-isect: x:A ⋂ B[x],
church-Nat: cNat,
church-inductive: church-inductive{i:l}(x)
FDL editor aliases :
indNat
Latex:
INat == x:cNat \mcap{} church-inductive\{i:l\}(x)
Date html generated:
2020_05_20-AM-08_05_43
Last ObjectModification:
2019_11_15-PM-10_36_58
Theory : general
Home
Index