Closure spaces before topology

Statement

A closure space is a set with an extensive, monotone and idempotent operation on its subsets that sends the empty set to the empty set. Preservation of finite unions is a separate condition.

Definition

Let be a set and let denote its power set, ordered by inclusion. A closure space on consists of a map satisfying, for all ,

A subset is closed when . The first three axioms say that is a closure operator on the ordered set ; the fourth supplies the empty-set condition.

The cited intersection theorem gives the useful equivalent description

Indeed, is closed and contains , and monotonicity puts it inside every closed superset of . Thus is the smallest closed set containing .

Assumptions

The underlying set is arbitrary and may be empty. To specify a closure space, one supplies the map and the four displayed properties. No topology, metric or separation condition on is required.

Conclusion

The resulting structure provides a closure operation and a notion of closed subset, with arbitrary intersections of closed sets again closed. A topological closure requires the additional identity

This extra condition is called topologizability in the cited source. It is not one of the four axioms above.

Main citations

• Exact structure and closure laws: ClosureSpace, lines 28–30; its operation and laws, lines 37–61.
• Closed intersections and closure minimality: ClosureSpace.closure_min, ClosureSpace.isClosed_sInter and ClosureSpace.closure_eq_sInter, lines 78–99.
• The additional finite-union condition: ClosureSpace.IsTopologizable, lines 102–103.
• The underlying order-theoretic structure: Mathlib ClosureOperator in Order/Closure.lean, at the pinned mathlib commit.
• Ryotaro Tanaka, arXiv:2504.05551v1, Definition 3.1 and Remark 3.4: the four axioms and the intersection description.

structure ClosureSpace (α : Type u) where
  toClosureOperator : ClosureOperator (Set α)
  map_empty' : toClosureOperator ∅ = ∅

structure ClosureSpace (α : Type u) where
  toClosureOperator : ClosureOperator (Set α)
  map_empty' : toClosureOperator ∅ = ∅

namespace ClosureSpace

variable {α : Type u}

/-- The underlying set closure. -/

structure ClosureSpace (α : Type u) where
  toClosureOperator : ClosureOperator (Set α)
  map_empty' : toClosureOperator ∅ = ∅

namespace ClosureSpace

variable {α : Type u}

/-- The underlying set closure. -/

structure ClosureSpace (α : Type u) where
  toClosureOperator : ClosureOperator (Set α)
  map_empty' : toClosureOperator ∅ = ∅

namespace ClosureSpace

variable {α : Type u}

/-- The underlying set closure. -/

structure ClosureSpace (α : Type u) where
  toClosureOperator : ClosureOperator (Set α)
  map_empty' : toClosureOperator ∅ = ∅

namespace ClosureSpace

variable {α : Type u}

/-- The underlying set closure. -/

structure ClosureOperator [Preorder α] extends α →o α where
  /-- An element is less than or equal its closure -/
  le_closure' : ∀ x, x ≤ toFun x
  /-- Closures are idempotent -/
  idempotent' : ∀ x, toFun (toFun x) = toFun x
  /-- Predicate for an element to be closed.

  By default, this is defined as `c.IsClosed x := (c x = x)` (see `isClosed_iff`).
  We allow an override to fix definitional equalities. -/
  IsClosed (x : α) : Prop := toFun x = x
  isClosed_iff {x : α} : IsClosed x ↔ toFun x = x := by aesop