Closed sets are elegantly described using coreflexives and inclusion
EndoRelationā āAā āR\textbf{EndoRelation} \; A \; REndoRelationAR
PowerSetā āAā āX\textbf{PowerSet} \; A \; XPowerSetAX
Ī¦X;RāR;Ī¦X\Phi_X ; R \subseteq R ; \Phi_XĪ¦Xā;RāR;Ī¦Xā
pred Closed(A: set univ, R: univ->univ, X: set univ) { EndoRelation[A,R] X in A X<:R in R:>X }
Last updated 8 months ago