Commit d57aaad5 authored by Michael Kohlhase's avatar Michael Kohlhase

comment is obsolete

parent ee18ee95
......@@ -13,7 +13,7 @@ theory neighborhoodSystem : base:?Logic =
isOpen : (set X) ⟶ bool ❘ = [S] ∀ [x] x ∈ S ⇒ ∃ [U] U ∈ (N x) ∧ U ⊑ S❙
// view ?topology_theory -> ?neighborhoodSystem =
// view topologyFromNHsystem: ?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