Nuprl Definition : set-predicate
set-predicate{i:l}(s;a.P[a]) == ∀a1,a2:coSet{i:l}. ((a1 ∈ s) ⇒ (a2 ∈ s) ⇒ seteq(a1;a2) ⇒ P[a1] ⇒ P[a2])
Definitions occuring in Statement :
setmem: (x ∈ s),
seteq: seteq(s1;s2),
coSet: coSet{i:l},
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions occuring in definition :
implies: P ⇒ Q,
seteq: seteq(s1;s2),
setmem: (x ∈ s),
coSet: coSet{i:l},
all: ∀x:A. B[x]
FDL editor aliases :
set-predicate
Latex:
set-predicate\{i:l\}(s;a.P[a]) ==
\mforall{}a1,a2:coSet\{i:l\}. ((a1 \mmember{} s) {}\mRightarrow{} (a2 \mmember{} s) {}\mRightarrow{} seteq(a1;a2) {}\mRightarrow{} P[a1] {}\mRightarrow{} P[a2])
Date html generated:
2018_07_29-AM-09_52_05
Last ObjectModification:
2018_07_18-AM-09_52_27
Theory : constructive!set!theory
Home
Index