Nuprl Definition : respects-equality
respects-equality(S;T) == ∀x,y:Base. ((x = y ∈ S) ⇒ (x ∈ T) ⇒ (x = y ∈ T))
Definitions occuring in Statement :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
base: Base,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
base: Base,
implies: P ⇒ Q,
member: t ∈ T,
equal: s = t ∈ T
FDL editor aliases :
respects-equality
Latex:
respects-equality(S;T) == \mforall{}x,y:Base. ((x = y) {}\mRightarrow{} (x \mmember{} T) {}\mRightarrow{} (x = y))
Date html generated:
2019_06_20-AM-11_13_38
Last ObjectModification:
2018_11_19-PM-10_02_48
Theory : core_2
Home
Index