Nuprl Definition : extend-type
(T)+ == x,y:Base//((x ∈ T ⇐⇒ y ∈ T) ∧ ((x ∈ T) ⇒ (x = y ∈ T)))
Definitions occuring in Statement :
quotient: x,y:A//B[x; y],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
and: P ∧ Q,
member: t ∈ T,
base: Base,
equal: s = t ∈ T
Definitions occuring in definition :
quotient: x,y:A//B[x; y],
base: Base,
and: P ∧ Q,
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
member: t ∈ T,
equal: s = t ∈ T
FDL editor aliases :
extend-type
Latex:
(T)+ == x,y:Base//((x \mmember{} T \mLeftarrow{}{}\mRightarrow{} y \mmember{} T) \mwedge{} ((x \mmember{} T) {}\mRightarrow{} (x = y)))
Date html generated:
2019_06_20-PM-00_33_23
Last ObjectModification:
2018_11_25-PM-06_34_10
Theory : quot_1
Home
Index