Nuprl Definition : inverse-letters
a = -b ==
∃x:X. (((a = (inl x) ∈ (X + X)) ∧ (b = (inr x ) ∈ (X + X))) ∨ ((a = (inr x ) ∈ (X + X)) ∧ (b = (inl x) ∈ (X + X))))
Definitions occuring in Statement :
exists: ∃x:A. B[x],
or: P ∨ Q,
and: P ∧ Q,
inr: inr x ,
inl: inl x,
union: left + right,
equal: s = t ∈ T
Definitions occuring in definition :
inl: inl x,
union: left + right,
equal: s = t ∈ T,
inr: inr x ,
and: P ∧ Q,
or: P ∨ Q,
exists: ∃x:A. B[x]
FDL editor aliases :
inverse-letters
Latex:
a = -b == \mexists{}x:X. (((a = (inl x)) \mwedge{} (b = (inr x ))) \mvee{} ((a = (inr x )) \mwedge{} (b = (inl x))))
Date html generated:
2017_01_19-PM-02_49_10
Last ObjectModification:
2017_01_13-PM-10_04_57
Theory : free!groups
Home
Index