Nuprl Definition : case-endpoints
[r=0 ⟶ a; r=1 ⟶ b] ==  (a ∨ b)
Definitions occuring in Statement : 
case-term: (u ∨ v)
, 
face-zero: (i=0)
Definitions occuring in definition : 
case-term: (u ∨ v)
, 
face-zero: (i=0)
FDL editor aliases : 
case-endpoints
Latex:
[r=0  \mvdash{}\mrightarrow{}  a;  r=1  \mvdash{}\mrightarrow{}  b]  ==    (a  \mvee{}  b)
Date html generated:
2016_07_08-PM-06_50_53
Last ObjectModification:
2016_06_23-PM-01_54_56
Theory : cubical!type!theory
Home
Index