Nuprl Definition : uimplies
This is "uniform" implication.
Evidence for (a ⇒ b) is a function from evidence for a to evidence for b,
but evidence for (b supposing a) is something that is evidence for b
as long as a is not empty (i.e. supposing that a has evidence).
Thus, the evidence must be "uniform" because it does not depend on
the the evidence for a. ⋅
b supposing a == ⋂:a. b
Definitions occuring in Statement :
isect: ⋂x:A. B[x]
Definitions occuring in definition :
isect: ⋂x:A. B[x]
Rules referencing :
Continuity,
StrongContinuity2
FDL editor aliases :
given
Latex:
b supposing a == \mcap{}:a. b
Date html generated:
2016_07_08-PM-04_46_32
Last ObjectModification:
2015_10_29-PM-06_57_40
Theory : core_2
Home
Index