TOPOLOGICAL CLOSURE

-type constructs the topological closure of a set, the smallest closed set containing it, by including all its limit points. It is fundamental in topology and analysis, supporting definitions of continuity and density.

In this system, operates over , leveraging and to define closure points, with Z3 ensuring rigorous verification in the context of Schwartz’s framework.

Formation

(-Formation). The closure of a set in a topological space (here, with the standard topology) forms a new set containing and its limit points.

type exp =
  | Closure of exp  (* cl(S) *)

Introduction

(-Introduction). The closure of is introduced as , the set of all points such that every neighborhood of intersects .

let closure_set (s : exp) : exp =
  Closure (s)

Elimination

(-Elimination). Membership in holds if a point is in or is a limit point of , i.e., approachable by a sequence in .

let reduce env ctx = function
  | App (Closure (Set (Lam (x, _, p))), y) ->
      Or (subst x y p,
          Exists ("a", Seq Real,
            And (Forall ("n", Nat, App (Set (Lam (x, Real, p)), App (Var "a", Var "n"))),
                 Limit (Var "a", Infinity, y, True))))
  | _ -> ...

Computation

(-Computation). Applying to a point reduces to checking membership or limit point status, verifiable by Z3 for concrete sequences and predicates.

let infer env ctx (Closure s) =
  check env ctx s (Set Real); Set Real

Uniqueness

(-Uniqueness). The closure is uniquely determined as the smallest closed set containing , equal to another set if , provable via .

let equal env ctx (Closure s1) (Closure s2) =
  equal env ctx s1 s2

Theorems

(Idempotence). The closure of a closure equals the closure: , as closure yields a closed set.

(Union Preservation). The closure of a union equals the union of closures: , reflecting topological properties over .

let closure_union (s : exp) (t : exp) =
  SetEq (Closure (Union (s, t)),
         Union (Closure s, Closure t))