Nuprl Definition : uall
This is "uniform" universal quantification.
Evidence for ⌜∀[x:A]. B[x]⌝ must be something that is a member of ⌜B[x]⌝
whenever ⌜x ∈ A⌝. Such evidence is independent of the choice of ⌜x ∈ A⌝. ⋅
∀[x:A]. B[x] == ⋂x:A. B[x]
Definitions occuring in Statement :
isect: ⋂x:A. B[x]
Definitions occuring in definition :
isect: ⋂x:A. B[x]
Rules referencing :
Continuity,
ispairCases,
isintCases,
isatomCases,
isaxiomCases,
islambdaCases,
isinlCases,
isinrCases,
isatom1Cases,
isatom2Cases,
lessCases,
uallFunctionality,
uallLevelFunctionality
FDL editor aliases :
uall
Latex:
\mforall{}[x:A]. B[x] == \mcap{}x:A. B[x]
Date html generated:
2016_07_08-PM-04_46_30
Last ObjectModification:
2015_10_29-PM-07_09_51
Theory : core_2
Home
Index