Closed

Closed sets are elegantly described using coreflexives and inclusion

Closedā€…ā€ŠAā€…ā€ŠRā€…ā€ŠX\textbf{Closed} \; A \; R \; X

EndoRelationā€…ā€ŠAā€…ā€ŠR\textbf{EndoRelation} \; A \; R

PowerSetā€…ā€ŠAā€…ā€ŠX\textbf{PowerSet} \; A \; X

Ī¦X;RāŠ†R;Ī¦X\Phi_X ; R \subseteq R ; \Phi_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