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