Commit 7cfafb8c authored by Michael Kohlhase's avatar Michael Kohlhase

playing with neighborhood systems

parent e4c1b1c8
namespace http://mathhub.info/MitM/smglom/topology ❚
import base http://mathhub.info/MitM/Foundation ❚
import sets http://mathhub.info/MitM/smglom/typedsets ❚
theory neighborhoodSystem : base:?Logic =
include sets:?filter ❙
universe : type ❘ # X ❙
nhsys : X ⟶ powerset (set X) ❘ # N ❙
axiom_filter : ⊦ ∀ [x] isFilter (N x)❙ // maybe better use a predicate subtype for N? ❙
axiom_nhsys1 : ⊦ ∀ [x] ∀ [U] U ∈ (N x) ⇒ x ∈ U ❙
axiom_nhsys2 : ⊦ ∀ [x] ∀ [U] U ∈ (N x) ⇒ ∃ [V] (N x) ∧ ∀ [y] y ∈ V ⇒ U ∈ (N y) ❙
isOpen : (set X) ⟶ bool ❘ = [S] ∀ [x] x ∈ S ⇒ ∃ [U] U ∈ (N x) ∧ U ⊑ S❙
// view ?topology_theory -> ?neighborhoodSystem =
// universe := universe ❙
// topology := isOpen ❙
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment