Nuprl Definition : coSet-bisimulation
coSet-bisimulation{i:l}(x,y.R[x; y]) ==
∀T:𝕌'
((((a:Type × (a ⟶ T)) ⊆r T) ∧ (coSet{i:l} ⊆r T))
⇒ (∀x,y:coSet{i:l}. (R[x; y] ⇒ (x = y ∈ T)))
⇒ (∀x,y:coSet{i:l}. (R[x; y] ⇒ (x = y ∈ (a:Type × (a ⟶ T))))))
Definitions occuring in Statement :
coSet: coSet{i:l},
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type,
equal: s = t ∈ T
Definitions occuring in definition :
and: P ∧ Q,
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
coSet: coSet{i:l},
implies: P ⇒ Q,
equal: s = t ∈ T,
product: x:A × B[x],
universe: Type,
function: x:A ⟶ B[x]
FDL editor aliases :
coSet-bisimulation
Latex:
coSet-bisimulation\{i:l\}(x,y.R[x; y]) ==
\mforall{}T:\mBbbU{}'
((((a:Type \mtimes{} (a {}\mrightarrow{} T)) \msubseteq{}r T) \mwedge{} (coSet\{i:l\} \msubseteq{}r T))
{}\mRightarrow{} (\mforall{}x,y:coSet\{i:l\}. (R[x; y] {}\mRightarrow{} (x = y)))
{}\mRightarrow{} (\mforall{}x,y:coSet\{i:l\}. (R[x; y] {}\mRightarrow{} (x = y))))
Date html generated:
2018_07_29-AM-09_49_46
Last ObjectModification:
2018_05_29-PM-05_50_57
Theory : constructive!set!theory
Home
Index