Theory topology

⊢ ∀s. ARBITRARY s ⇔ T

⊢ ∀P Q.
    P INTERSECTION_OF Q =
    (λs. ∃u. P u ∧ (∀c. c ∈ u ⇒ Q c) ∧ BIGINTER u = s)

⊢ ∀P Q. P UNION_OF Q = (λs. ∃u. P u ∧ (∀c. c ∈ u ⇒ Q c) ∧ BIGUNION u = s)

⊢ ∀s. closed s ⇔ closed_in s 𝕌(:α)

⊢ ∀top s.
    closed_in top s ⇔ s ⊆ topspace top ∧ open_in top (topspace top DIFF s)

⊢ ∀top s.
    top closure_of s =
    {x | x ∈ topspace top ∧ ∀t. x ∈ t ∧ open_in top t ⇒ ∃y. y ∈ s ∧ y ∈ t}

⊢ ∀top s.
    compact_in top s ⇔
    s ⊆ topspace top ∧
    ∀U. (∀u. u ∈ U ⇒ open_in top u) ∧ s ⊆ BIGUNION U ⇒
        ∃V. FINITE V ∧ V ⊆ U ∧ s ⊆ BIGUNION V

⊢ ∀top. compact_space top ⇔ compact_in top (topspace top)

⊢ ∀top top' f.
    continuous_map (top,top') f ⇔
    (∀x. x ∈ topspace top ⇒ f x ∈ topspace top') ∧
    ∀u. open_in top' u ⇒ open_in top {x | x ∈ topspace top ∧ f x ∈ u}

⊢ ∀top s.
    top derived_set_of s =
    {x |
     x ∈ topspace top ∧
     ∀t. x ∈ t ∧ open_in top t ⇒ ∃y. y ≠ x ∧ y ∈ s ∧ y ∈ t}

⊢ ∀top s. top frontier_of s = top closure_of s DIFF top interior_of s

⊢ ∀P s. P hull s = BIGINTER {t | P t ∧ s ⊆ t}

⊢ ∀top s. top interior_of s = {x | ∃t. open_in top t ∧ x ∈ t ∧ t ⊆ s}

⊢ ∀L. istopology L ⇔
      ∅ ∈ L ∧ (∀s t. s ∈ L ∧ t ∈ L ⇒ s ∩ t ∈ L) ∧
      ∀k. k ⊆ L ⇒ BIGUNION k ∈ L

⊢ ∀top x S'.
    limpt top x S' ⇔
    x ∈ topspace top ∧ ∀N. neigh top (N,x) ⇒ ∃y. x ≠ y ∧ S' y ∧ N y

⊢ ∀top N x.
    neigh top (N,x) ⇔ ∃P. open_in top P ∧ P ⊆ N ∧ P x ∧ N ⊆ topspace top

⊢ ∀s. open s ⇔ open_in s 𝕌(:α)

⊢ ∀r s. pairwiseD r s ⇔ ∀x y. x ∈ s ∧ y ∈ s ∧ x ≠ y ⇒ r x y

⊢ ∀P s t. (P relative_to s) t ⇔ ∃u. P u ∧ s ∩ u = t

⊢ ∀top u. subtopology top u = topology {s ∩ u | open_in top s}

⊢ ∀top top' f x.
    topcontinuous_at top top' f x ⇔
    x ∈ topspace top ∧ (∀x. x ∈ topspace top ⇒ f x ∈ topspace top') ∧
    ∀v. open_in top' v ∧ f x ∈ v ⇒
        ∃u. open_in top u ∧ x ∈ u ∧ ∀y. y ∈ u ⇒ f y ∈ v

⊢ ∃rep. TYPE_DEFINITION istopology rep

⊢ (∀a. topology (open_in a) = a) ∧
  ∀r. istopology r ⇔ open_in (topology r) = r

⊢ ∀top. topspace top = BIGUNION {s | open_in top s}

⊢ ∀P s.
    (ARBITRARY INTERSECTION_OF P) s ⇔
    (ARBITRARY UNION_OF (λs. P (𝕌(:α) DIFF s))) (𝕌(:α) DIFF s)

⊢ ∀P. (ARBITRARY INTERSECTION_OF P) 𝕌(:α)

⊢ ∀P. ARBITRARY INTERSECTION_OF ARBITRARY INTERSECTION_OF P =
      ARBITRARY INTERSECTION_OF P

⊢ ∀P s. P s ⇒ (ARBITRARY INTERSECTION_OF P) s

⊢ ∀P s t.
    (ARBITRARY INTERSECTION_OF P) s ∧ (ARBITRARY INTERSECTION_OF P) t ⇒
    (ARBITRARY INTERSECTION_OF P) (s ∩ t)

⊢ ∀P u.
    (∀s. s ∈ u ⇒ (ARBITRARY INTERSECTION_OF P) s) ⇒
    (ARBITRARY INTERSECTION_OF P) (BIGINTER u)

⊢ ∀P u.
    ARBITRARY INTERSECTION_OF P relative_to u =
    ARBITRARY INTERSECTION_OF (P relative_to u) relative_to u

⊢ ∀P. (∀s t. P s ∧ P t ⇒ P (s ∪ t)) ⇒
      ∀s t.
        (ARBITRARY INTERSECTION_OF P) s ∧ (ARBITRARY INTERSECTION_OF P) t ⇒
        (ARBITRARY INTERSECTION_OF P) (s ∪ t)

⊢ ∀P. (∀s t.
         (ARBITRARY INTERSECTION_OF P) s ∧ (ARBITRARY INTERSECTION_OF P) t ⇒
         (ARBITRARY INTERSECTION_OF P) (s ∪ t)) ⇔
      ∀s t. P s ∧ P t ⇒ (ARBITRARY INTERSECTION_OF P) (s ∪ t)

⊢ ∀B s. (ARBITRARY UNION_OF B) s ⇔ ∀x. x ∈ s ⇒ ∃u. u ∈ B ∧ x ∈ u ∧ u ⊆ s

⊢ ∀P s.
    (ARBITRARY UNION_OF P) s ⇔
    (ARBITRARY INTERSECTION_OF (λs. P (𝕌(:α) DIFF s))) (𝕌(:α) DIFF s)

⊢ ∀P. (ARBITRARY UNION_OF P) ∅

⊢ ∀P. ARBITRARY UNION_OF ARBITRARY UNION_OF P = ARBITRARY UNION_OF P

⊢ ∀P s. P s ⇒ (ARBITRARY UNION_OF P) s

⊢ ∀P. (∀s t. P s ∧ P t ⇒ P (s ∩ t)) ⇒
      ∀s t.
        (ARBITRARY UNION_OF P) s ∧ (ARBITRARY UNION_OF P) t ⇒
        (ARBITRARY UNION_OF P) (s ∩ t)

⊢ ∀P. (∀s t.
         (ARBITRARY UNION_OF P) s ∧ (ARBITRARY UNION_OF P) t ⇒
         (ARBITRARY UNION_OF P) (s ∩ t)) ⇔
      ∀s t. P s ∧ P t ⇒ (ARBITRARY UNION_OF P) (s ∩ t)

⊢ ∀u. ARBITRARY UNION_OF (λs. FINITE s ∧ s ≠ ∅) INTERSECTION_OF u =
      ARBITRARY UNION_OF (FINITE INTERSECTION_OF u relative_to BIGUNION u)

⊢ ∀P u.
    ARBITRARY UNION_OF P relative_to u =
    ARBITRARY UNION_OF (P relative_to u)

⊢ ∀P s t.
    (ARBITRARY UNION_OF P) s ∧ (ARBITRARY UNION_OF P) t ⇒
    (ARBITRARY UNION_OF P) (s ∪ t)

⊢ ∀P u.
    (∀s. s ∈ u ⇒ (ARBITRARY UNION_OF P) s) ⇒
    (ARBITRARY UNION_OF P) (BIGUNION u)

⊢ ∀s t. BIGUNION {s; t} = s ∪ t

⊢ A ⊆ ARBITRARY UNION_OF P ⇒ BIGUNION A ∈ ARBITRARY UNION_OF P

⊢ ∀top s.
    closed_in top s ∧ open_in top s ⇔
    s ⊆ topspace top ∧ top frontier_of s = ∅

⊢ ∀top k c. compact_in top k ∧ c ⊆ k ∧ closed_in top c ⇒ compact_in top c

⊢ ∀top k.
    k ≠ ∅ ∧ (∀s. s ∈ k ⇒ closed_in top s) ⇒ closed_in top (BIGINTER k)

⊢ ∀top s.
    FINITE s ∧ (∀t. t ∈ s ⇒ closed_in top t) ⇒ closed_in top (BIGUNION s)

⊢ ∀top s. closed_in top (top closure_of s)

⊢ ∀top s. compact_space top ∧ closed_in top s ⇒ compact_in top s

⊢ ∀top s. closed_in top s ⇔ top derived_set_of s ⊆ s ∧ s ⊆ topspace top

⊢ ∀f top top' c.
    continuous_map (top,top') f ∧ closed_in top' c ⇒
    closed_in top {x | x ∈ topspace top ∧ f x ∈ c}

⊢ ∀f top top' u v.
    continuous_map (top,top') f ∧ closed_in top u ∧ closed_in top' v ⇒
    closed_in top {x | x ∈ u ∧ f x ∈ v}

⊢ ∀top s t.
    closed_in (subtopology top t) s ⇔
    s ⊆ topspace top ∧ s ⊆ t ∧ ∀x. x ∈ top derived_set_of s ∧ x ∈ t ⇒ x ∈ s

⊢ ∀top s t. closed_in top s ∧ open_in top t ⇒ closed_in top (s DIFF t)

⊢ ∀top. closed_in top ∅

⊢ ∀top s. closed_in top (top frontier_of s)

⊢ ∀top s t. closed_in (subtopology top s) t ⇒ t ⊆ s

⊢ ∀top s t. closed_in top s ∧ closed_in top t ⇒ closed_in top (s ∩ t)

⊢ ∀top s t. closed_in (subtopology top s) t ⇔ s ∩ top closure_of t = t

⊢ ∀top. closed top ⇒ ∀s. closed_in top s ⇔ open_in top (COMPL s)

⊢ ∀top s. closed_in top relative_to s = closed_in (subtopology top s)

⊢ ∀top s. closed_in top s ⇒ s ⊆ topspace top

⊢ ∀top u s.
    closed_in (subtopology top u) s ⇔ ∃t. closed_in top t ∧ s = t ∩ u

⊢ ∀top s. closed_in (subtopology top ∅) s ⇔ s = ∅

⊢ ∀top u. closed_in (subtopology top u) u ⇔ u ⊆ topspace top

⊢ ∀top s t u.
    closed_in (subtopology top t) s ∧ closed_in (subtopology top u) s ⇒
    closed_in (subtopology top (t ∪ u)) s

⊢ ∀top. closed_in top (topspace top)

⊢ ∀top s t. closed_in top s ∧ closed_in top t ⇒ closed_in top (s ∪ t)

⊢ ∀top. closed top ⇒ ∀S'. closed_in top S' ⇔ ∀x. limpt top x S' ⇒ S' x

⊢ ∀top s. top closure_of s = topspace top ∩ (s ∪ top derived_set_of s)

⊢ ∀top s. top closure_of s = topspace top ∩ s ∪ top derived_set_of s

⊢ ∀top s. closed_in top s ⇒ top closure_of s = s

⊢ ∀top s. top closure_of top closure_of s = top closure_of s

⊢ ∀top s.
    top closure_of (topspace top DIFF s) =
    topspace top DIFF top interior_of s

⊢ ∀top. top closure_of ∅ = ∅

⊢ ∀top s. top closure_of s = s ⇔ closed_in top s

⊢ ∀top s. s ⊆ topspace top ⇒ (top closure_of s = ∅ ⇔ s = ∅)

⊢ ∀top s. top closure_of s = ∅ ⇔ DISJOINT (topspace top) s

⊢ ∀top s.
    top closure_of s = topspace top ⇔
    top interior_of (topspace top DIFF s) = ∅

⊢ ∀top s. s ⊆ topspace top ⇒ top closure_of s = closed_in top hull s

⊢ ∀top s.
    top closure_of s =
    topspace top DIFF top interior_of (topspace top DIFF s)

⊢ ∀top s t. s ⊆ t ∧ closed_in top t ⇒ top closure_of s ⊆ t

⊢ ∀top s t.
    s ⊆ topspace top ∧ closed_in top t ⇒ (top closure_of s ⊆ t ⇔ s ⊆ t)

⊢ ∀top s t. s ⊆ t ⇒ top closure_of s ⊆ top closure_of t

⊢ ∀top s t.
    open_in top s ⇒
    top closure_of (s ∩ top closure_of t) = top closure_of (s ∩ t)

⊢ ∀top s t.
    open_in top s ∧ s ⊆ top closure_of t ⇒
    top closure_of (s ∩ t) = top closure_of s

⊢ ∀top s t u.
    open_in (subtopology top u) s ∧ t ⊆ u ⇒
    top closure_of (s ∩ top closure_of t) = top closure_of (s ∩ t)

⊢ ∀top s. top closure_of s = top closure_of (topspace top ∩ s)

⊢ ∀top s. s ⊆ topspace top ⇒ s ⊆ top closure_of s

⊢ ∀top s. s ⊆ topspace top ∧ top closure_of s ⊆ s ⇔ closed_in top s

⊢ ∀top s. topspace top ∩ s ⊆ top closure_of s

⊢ ∀top s t. subtopology top s closure_of t ⊆ s

⊢ ∀top s. top closure_of s ⊆ topspace top

⊢ ∀top u s. subtopology top u closure_of s = u ∩ top closure_of (u ∩ s)

⊢ ∀top s t u.
    t ⊆ u ⇒ subtopology top t closure_of s ⊆ subtopology top u closure_of s

⊢ ∀top u s.
    open_in top u ∨ s ⊆ u ⇒
    subtopology top u closure_of s = u ∩ top closure_of s

⊢ ∀top s u. subtopology top u closure_of s ⊆ top closure_of s

⊢ ∀top. top closure_of topspace top = topspace top

⊢ ∀top s t. top closure_of (s ∪ t) = top closure_of s ∪ top closure_of t

⊢ ∀top f.
    FINITE f ⇒
    top closure_of BIGUNION f = BIGUNION {top closure_of s | s ∈ f}

⊢ ∀top s t.
    s ⊆ t ∧ closed_in top t ∧ (∀t'. s ⊆ t' ∧ closed_in top t' ⇒ t ⊆ t') ⇒
    top closure_of s = t

⊢ ∀top. top closure_of 𝕌(:α) = topspace top

⊢ ∀top s. compact_in (subtopology top s) s ⇔ compact_in top s

⊢ ∀top top'.
    topspace top' = topspace top ∧ (∀u. open_in top u ⇒ open_in top' u) ⇒
    ∀s. compact_in top' s ⇒ compact_in top s

⊢ ∀top. compact_in top ∅

⊢ ∀top a. compact_in top {a} ⇔ a ∈ topspace top

⊢ ∀top s. compact_in top s ⇒ s ⊆ topspace top

⊢ ∀top s.
    compact_in top s ⇔ s ⊆ topspace top ∧ compact_space (subtopology top s)

⊢ ∀top s t. compact_in (subtopology top s) t ⇔ compact_in top t ∧ t ⊆ s

⊢ ∀top.
    compact_space top ⇔
    ∀U. (∀u. u ∈ U ⇒ open_in top u) ∧ BIGUNION U = topspace top ⇒
        ∃V. FINITE V ∧ V ⊆ U ∧ BIGUNION V = topspace top

⊢ ∀top.
    compact_space top ⇔
    ∀U. (∀u. u ∈ U ⇒ open_in top u) ∧ topspace top ⊆ BIGUNION U ⇒
        ∃V. FINITE V ∧ V ⊆ U ∧ topspace top ⊆ BIGUNION V

⊢ ∀top top'.
    topspace top' = topspace top ∧ (∀u. open_in top u ⇒ open_in top' u) ⇒
    compact_space top' ⇒
    compact_space top

⊢ ∀top s. compact_in top s ⇒ compact_space (subtopology top s)

⊢ ∀top. topspace top = ∅ ⇒ compact_space top

⊢ ∀s. 𝕌(:α) DIFF (𝕌(:α) DIFF s) = s

⊢ ∀top top' f.
    continuous_map (top,top') f ⇔
    IMAGE f (topspace top) ⊆ topspace top' ∧
    ∀u. open_in top' u ⇒ open_in top {x | x ∈ topspace top ∧ f x ∈ u}

⊢ ∀top top' f.
    continuous_map (top,top') f ⇔
    (∀x. x ∈ topspace top ⇒ f x ∈ topspace top') ∧
    ∀c. closed_in top' c ⇒ closed_in top {x | x ∈ topspace top ∧ f x ∈ c}

⊢ ∀top top' top'' f g.
    continuous_map (top,top') f ∧ continuous_map (top',top'') g ⇒
    continuous_map (top,top'') (g ∘ f)

⊢ ∀top1 top2 c.
    continuous_map (top1,top2) (λx. c) ⇔
    topspace top1 = ∅ ∨ c ∈ topspace top2

⊢ ∀top top' f g.
    (∀x. x ∈ topspace top ⇒ f x = g x) ∧ continuous_map (top,top') f ⇒
    continuous_map (top,top') g

⊢ ∀top top' f.
    continuous_map (top,top') f ⇔
    ∀x. x ∈ topspace top ⇒ topcontinuous_at top top' f x

⊢ ∀top top' f s.
    continuous_map (top,top') f ⇒ continuous_map (subtopology top s,top') f

⊢ ∀top top' f s t.
    continuous_map (subtopology top t,top') f ∧ s ⊆ t ⇒
    continuous_map (subtopology top s,top') f

⊢ ∀top. continuous_map (top,top) (λx. x)

⊢ ∀top top' f.
    continuous_map (top,top') f ⇒ IMAGE f (topspace top) ⊆ topspace top'

⊢ ∀top top' f.
    topspace top' = ∅ ⇒ (continuous_map (top,top') f ⇔ topspace top = ∅)

⊢ ∀top top' f t.
    continuous_map (top,subtopology top' t) f ⇒ continuous_map (top,top') f

⊢ ∀top top' f t.
    continuous_map (top,top') f ∧ IMAGE f (topspace top) ⊆ t ⇒
    continuous_map (top,subtopology top' t) f

⊢ ∀top top' s f.
    continuous_map (top,subtopology top' s) f ⇔
    continuous_map (top,top') f ∧ IMAGE f (topspace top) ⊆ s

⊢ ∀top top' f. topspace top = ∅ ⇒ continuous_map (top,top') f

⊢ ∀P. (countable ∩ pairwiseD DISJOINT) UNION_OF
      (countable ∩ pairwiseD DISJOINT) UNION_OF P =
      (countable ∩ pairwiseD DISJOINT) UNION_OF P

⊢ ∀P s.
    (countable INTERSECTION_OF P) s ⇔
    (countable UNION_OF (λs. P (𝕌(:α) DIFF s))) (𝕌(:α) DIFF s)

⊢ ∀P. (countable INTERSECTION_OF P) 𝕌(:α)

⊢ ∀P. countable INTERSECTION_OF countable INTERSECTION_OF P =
      countable INTERSECTION_OF P

⊢ ∀P s. P s ⇒ (countable INTERSECTION_OF P) s

⊢ ∀P s t.
    (countable INTERSECTION_OF P) s ∧ (countable INTERSECTION_OF P) t ⇒
    (countable INTERSECTION_OF P) (s ∩ t)

⊢ ∀P u.
    countable u ∧ (∀s. s ∈ u ⇒ (countable INTERSECTION_OF P) s) ⇒
    (countable INTERSECTION_OF P) (BIGINTER u)

⊢ ∀P u.
    countable INTERSECTION_OF P relative_to u =
    countable INTERSECTION_OF (P relative_to u) relative_to u

⊢ ∀P u s.
    P u ⇒
    ((countable INTERSECTION_OF P relative_to u) s ⇔
     (countable INTERSECTION_OF P) s ∧ s ⊆ u)

⊢ ∀P. (∀s t. P s ∧ P t ⇒ P (s ∪ t)) ⇒
      ∀s t.
        (countable INTERSECTION_OF P) s ∧ (countable INTERSECTION_OF P) t ⇒
        (countable INTERSECTION_OF P) (s ∪ t)

⊢ ∀P u.
    (countable INTERSECTION_OF P) ∅ ∧ (∀s t. P s ∧ P t ⇒ P (s ∪ t)) ∧
    FINITE u ∧ (∀s. s ∈ u ⇒ (countable INTERSECTION_OF P) s) ⇒
    (countable INTERSECTION_OF P) (BIGUNION u)

⊢ ∀P u.
    (∀s t. P s ∧ P t ⇒ P (s ∪ t)) ∧ FINITE u ∧ u ≠ ∅ ∧
    (∀s. s ∈ u ⇒ (countable INTERSECTION_OF P) s) ⇒
    (countable INTERSECTION_OF P) (BIGUNION u)

⊢ ∀P. (∀s t.
         (countable INTERSECTION_OF P) s ∧ (countable INTERSECTION_OF P) t ⇒
         (countable INTERSECTION_OF P) (s ∪ t)) ⇔
      ∀s t. P s ∧ P t ⇒ (countable INTERSECTION_OF P) (s ∪ t)

⊢ ∀s. countable s

⊢ ∀P s.
    P ∅ ∧ (∀t u. P t ∧ P u ⇒ P (t ∪ u)) ⇒
    ((countable UNION_OF P) s ⇔
     ∃t. (∀n. P (t n)) ∧ (∀n. t n ⊆ t (SUC n)) ∧
         BIGUNION {t n | n ∈ 𝕌(:num)} = s)

⊢ ∀P s.
    (countable UNION_OF P) s ⇔
    (countable INTERSECTION_OF (λs. P (𝕌(:α) DIFF s))) (𝕌(:α) DIFF s)

⊢ ∀P. (countable UNION_OF P) ∅

⊢ ∀P s.
    P ∅ ⇒
    ((countable UNION_OF P) s ⇔
     ∃t. (∀n. P (t n)) ∧ BIGUNION {t n | n ∈ 𝕌(:num)} = s)

⊢ ∀P. countable UNION_OF countable UNION_OF P = countable UNION_OF P

⊢ ∀P s. P s ⇒ (countable UNION_OF P) s

⊢ ∀P. (∀s t. P s ∧ P t ⇒ P (s ∩ t)) ⇒
      ∀s t.
        (countable UNION_OF P) s ∧ (countable UNION_OF P) t ⇒
        (countable UNION_OF P) (s ∩ t)

⊢ ∀P u.
    (countable UNION_OF P) 𝕌(:α) ∧ (∀s t. P s ∧ P t ⇒ P (s ∩ t)) ∧
    FINITE u ∧ (∀s. s ∈ u ⇒ (countable UNION_OF P) s) ⇒
    (countable UNION_OF P) (BIGINTER u)

⊢ ∀P u.
    (∀s t. P s ∧ P t ⇒ P (s ∩ t)) ∧ FINITE u ∧ u ≠ ∅ ∧
    (∀s. s ∈ u ⇒ (countable UNION_OF P) s) ⇒
    (countable UNION_OF P) (BIGINTER u)

⊢ ∀P. (∀s t.
         (countable UNION_OF P) s ∧ (countable UNION_OF P) t ⇒
         (countable UNION_OF P) (s ∩ t)) ⇔
      ∀s t. P s ∧ P t ⇒ (countable UNION_OF P) (s ∩ t)

⊢ ∀P u.
    countable UNION_OF P relative_to u =
    countable UNION_OF (P relative_to u)

⊢ ∀P s t.
    (countable UNION_OF P) s ∧ (countable UNION_OF P) t ⇒
    (countable UNION_OF P) (s ∪ t)

⊢ ∀P u.
    countable u ∧ (∀s. s ∈ u ⇒ (countable UNION_OF P) s) ⇒
    (countable UNION_OF P) (BIGUNION u)

⊢ ∀top s.
    top closure_of s = topspace top ⇔ ∀t. open_in top t ∧ t ≠ ∅ ⇒ s ∩ t ≠ ∅

⊢ ∀top. top derived_set_of ∅ = ∅

⊢ ∀top s t. s ⊆ t ⇒ top derived_set_of s ⊆ top derived_set_of t

⊢ ∀top s. top derived_set_of s = top derived_set_of (topspace top ∩ s)

⊢ ∀top s. top derived_set_of s ⊆ top closure_of s

⊢ ∀top s t. subtopology top s derived_set_of t ⊆ s

⊢ ∀top s. top derived_set_of s ⊆ topspace top

⊢ ∀top u s.
    subtopology top u derived_set_of s = u ∩ top derived_set_of (u ∩ s)

⊢ ∀top.
    top derived_set_of topspace top =
    {x | x ∈ topspace top ∧ ¬open_in top {x}}

⊢ ∀top s t.
    top derived_set_of (s ∪ t) =
    top derived_set_of s ∪ top derived_set_of t

⊢ ∀top f.
    FINITE f ⇒
    top derived_set_of BIGUNION f = BIGUNION {top derived_set_of s | s ∈ f}

⊢ ∀top s. s ⊆ topspace top ⇒ (top derived_set_of s ⊆ s ⇔ closed_in top s)

⊢ ∀top s. top derived_set_of s ⊆ s ⇔ closed_in top (topspace top ∩ s)

⊢ ∀u s. u DIFF BIGINTER s = BIGUNION {u DIFF t | t ∈ s}

⊢ ∀u s. u DIFF BIGUNION s = u ∩ BIGINTER {u DIFF t | t ∈ s}

⊢ ∀u s. s ≠ ∅ ⇒ u DIFF BIGUNION s = BIGINTER {u DIFF t | t ∈ s}

⊢ {x | F} = ∅

⊢ ∅ ∈ ARBITRARY UNION_OF P

⊢ ∀t1 t2. (t1 ⇔ t2) ⇒ t1 ⇒ t2

⊢ ∀P f s.
    (∃t. FINITE t ∧ t ⊆ IMAGE f s ∧ P t) ⇔
    ∃t. FINITE t ∧ t ⊆ s ∧ P (IMAGE f t)

⊢ ∀P f s.
    (∃t. FINITE t ∧ t ⊆ IMAGE f s ∧ P t) ⇔
    ∃t. FINITE t ∧ t ⊆ s ∧ (∀x y. x ∈ t ∧ y ∈ t ⇒ (f x = f y ⇔ x = y)) ∧
        P (IMAGE f t)

⊢ ∀P f s. (∃t. t ⊆ IMAGE f s ∧ P t) ⇔ ∃t. t ⊆ s ∧ P (IMAGE f t)

⊢ ∀P f s.
    (∃t. t ⊆ IMAGE f s ∧ P t) ⇔
    ∃t. t ⊆ s ∧ (∀x y. x ∈ t ∧ y ∈ t ⇒ (f x = f y ⇔ x = y)) ∧ P (IMAGE f t)

⊢ ∀P Q. (∀x. x ∈ P ⇒ ∃y. Q x y) ⇔ ∃f. ∀x. x ∈ P ⇒ Q x (f x)

⊢ ∀P Q. (∀x. P x ⇒ ∃y. Q x y) ⇔ ∃f. ∀x. P x ⇒ Q x (f x)

⊢ ∀s. FINITE s ⇒ ∀f. FINITE (IMAGE f s)

⊢ ∀top s. s ⊆ topspace top ∧ FINITE s ⇒ compact_in top s

⊢ ∀top s. FINITE s ⇒ (compact_in top s ⇔ s ⊆ topspace top)

⊢ ∀P s.
    (FINITE INTERSECTION_OF P) s ⇔
    (FINITE UNION_OF (λs. P (𝕌(:α) DIFF s))) (𝕌(:α) DIFF s)

⊢ ∀P. (FINITE INTERSECTION_OF P) 𝕌(:α)

⊢ ∀P. FINITE INTERSECTION_OF FINITE INTERSECTION_OF P =
      FINITE INTERSECTION_OF P

⊢ ∀P s. P s ⇒ (FINITE INTERSECTION_OF P) s

⊢ ∀P s t.
    (FINITE INTERSECTION_OF P) s ∧ (FINITE INTERSECTION_OF P) t ⇒
    (FINITE INTERSECTION_OF P) (s ∩ t)

⊢ ∀P u.
    FINITE u ∧ (∀s. s ∈ u ⇒ (FINITE INTERSECTION_OF P) s) ⇒
    (FINITE INTERSECTION_OF P) (BIGINTER u)

⊢ ∀P u.
    FINITE INTERSECTION_OF P relative_to u =
    FINITE INTERSECTION_OF (P relative_to u) relative_to u

⊢ ∀P u s.
    P u ⇒
    ((FINITE INTERSECTION_OF P relative_to u) s ⇔
     (FINITE INTERSECTION_OF P) s ∧ s ⊆ u)

⊢ ∀P. (∀s t. P s ∧ P t ⇒ P (s ∪ t)) ⇒
      ∀s t.
        (FINITE INTERSECTION_OF P) s ∧ (FINITE INTERSECTION_OF P) t ⇒
        (FINITE INTERSECTION_OF P) (s ∪ t)

⊢ ∀P. (∀s t.
         (FINITE INTERSECTION_OF P) s ∧ (FINITE INTERSECTION_OF P) t ⇒
         (FINITE INTERSECTION_OF P) (s ∪ t)) ⇔
      ∀s t. P s ∧ P t ⇒ (FINITE INTERSECTION_OF P) (s ∪ t)

⊢ ∀s t. FINITE s ∧ t ⊆ s ⇒ FINITE t

⊢ ∀P s.
    (FINITE UNION_OF P) s ⇔
    (FINITE INTERSECTION_OF (λs. P (𝕌(:α) DIFF s))) (𝕌(:α) DIFF s)

⊢ ∀P. (FINITE UNION_OF P) ∅

⊢ ∀P. FINITE UNION_OF FINITE UNION_OF P = FINITE UNION_OF P

⊢ ∀P s. P s ⇒ (FINITE UNION_OF P) s

⊢ ∀P. (∀s t. P s ∧ P t ⇒ P (s ∩ t)) ⇒
      ∀s t.
        (FINITE UNION_OF P) s ∧ (FINITE UNION_OF P) t ⇒
        (FINITE UNION_OF P) (s ∩ t)

⊢ ∀P. (∀s t.
         (FINITE UNION_OF P) s ∧ (FINITE UNION_OF P) t ⇒
         (FINITE UNION_OF P) (s ∩ t)) ⇔
      ∀s t. P s ∧ P t ⇒ (FINITE UNION_OF P) (s ∩ t)

⊢ ∀P u. FINITE UNION_OF P relative_to u = FINITE UNION_OF (P relative_to u)

⊢ ∀P s t.
    (FINITE UNION_OF P) s ∧ (FINITE UNION_OF P) t ⇒
    (FINITE UNION_OF P) (s ∪ t)

⊢ ∀P u.
    FINITE u ∧ (∀s. s ∈ u ⇒ (FINITE UNION_OF P) s) ⇒
    (FINITE UNION_OF P) (BIGUNION u)

⊢ ∀P f s.
    (∀t. FINITE t ∧ t ⊆ IMAGE f s ⇒ P t) ⇔
    ∀t. FINITE t ∧ t ⊆ s ⇒ P (IMAGE f t)

⊢ ∀P f s.
    (∀t. FINITE t ∧ t ⊆ IMAGE f s ⇒ P t) ⇔
    ∀t. FINITE t ∧ t ⊆ s ∧ (∀x y. x ∈ t ∧ y ∈ t ⇒ (f x = f y ⇔ x = y)) ⇒
        P (IMAGE f t)

⊢ (∀s. (P INTERSECTION_OF Q) s ⇒ R s) ⇔
  ∀t. P t ∧ (∀c. c ∈ t ⇒ Q c) ⇒ R (BIGINTER t)

⊢ ∀top P s.
    (∀x. x ∈ s ⇒ P x) ∧ closed_in top {x | x ∈ topspace top ∧ P x} ⇒
    ∀x. x ∈ top closure_of s ⇒ P x

⊢ ∀top P s.
    (∀x. x ∈ s ⇒ P x) ∧ closed_in top {x | x ∈ top closure_of s ∧ P x} ⇒
    ∀x. x ∈ top closure_of s ⇒ P x

⊢ ∀top P s.
    (∀x. x ∈ s ⇒ P x) ∧ closed_in top {x | P x} ⇒
    ∀x. x ∈ top closure_of s ⇒ P x

⊢ (∀s. (P relative_to u) s ⇒ Q s) ⇔ ∀s. P s ⇒ Q (u ∩ s)

⊢ ∀P f s. (∀t. t ⊆ IMAGE f s ⇒ P t) ⇔ ∀t. t ⊆ s ⇒ P (IMAGE f t)

⊢ ∀P f s.
    (∀t. t ⊆ IMAGE f s ⇒ P t) ⇔
    ∀t. t ⊆ s ∧ (∀x y. x ∈ t ∧ y ∈ t ⇒ (f x = f y ⇔ x = y)) ⇒ P (IMAGE f t)

⊢ (∀s. (P UNION_OF Q) s ⇒ R s) ⇔
  ∀t. P t ∧ (∀c. c ∈ t ⇒ Q c) ⇒ R (BIGUNION t)

⊢ ∀P a. (∀x. a = x ⇒ P x) ⇔ P a

⊢ ∀P a. (∀x. x = a ⇒ P x) ⇔ P a

⊢ ∀top s.
    top frontier_of s =
    top closure_of s ∩ top closure_of (topspace top DIFF s)

⊢ ∀top. top frontier_of ∅ = ∅

⊢ ∀top s.
    s ⊆ topspace top ⇒
    (top frontier_of s = ∅ ⇔ closed_in top s ∧ open_in top s)

⊢ ∀top s. open_in top s ⇒ top frontier_of s = top closure_of s DIFF s

⊢ ∀top s u.
    open_in top u ∧ u ∩ top frontier_of s ≠ ∅ ⇒ u ∩ s ≠ ∅ ∧ u DIFF s ≠ ∅

⊢ ∀top s. top frontier_of s = top frontier_of (topspace top ∩ s)

⊢ ∀top s. closed_in top s ⇒ top frontier_of s ⊆ s

⊢ ∀top s. s ⊆ topspace top ⇒ (top frontier_of s ⊆ s ⇔ closed_in top s)

⊢ ∀top s t. subtopology top s frontier_of t ⊆ s

⊢ ∀top s. top frontier_of s ⊆ topspace top

⊢ ∀top s t u.
    s ⊆ t ∧ t ⊆ u ⇒
    subtopology top t frontier_of s ⊆ subtopology top u frontier_of s

⊢ ∀top s u. u ∩ subtopology top u frontier_of s ⊆ top frontier_of s

⊢ ∀top. top frontier_of topspace top = ∅

⊢ ∀P s t.
    (∀f. (∀s. s ∈ f ⇒ P s) ⇒ P (BIGINTER f)) ∧ s ⊆ P hull t ∧ t ⊆ P hull s ⇒
    P hull s = P hull t

⊢ ∀P Q s. P ⊆ Q ⇒ Q hull s ⊆ P hull s

⊢ ∀P s. (∀f. (∀s. s ∈ f ⇒ P s) ⇒ P (BIGINTER f)) ⇒ (P hull s = s ⇔ P s)

⊢ ∀P s. P hull (P hull s) = P hull s

⊢ ∀P f s.
    (∀s. P (P hull s)) ∧ (∀s. P (IMAGE f s) ⇔ P s) ∧
    (∀x y. f x = f y ⇒ x = y) ∧ (∀y. ∃x. f x = y) ⇒
    P hull IMAGE f s = IMAGE f (P hull s)

⊢ ∀P f g s.
    (∀s. P (P hull s)) ∧ (∀s. P s ⇒ P (IMAGE f s)) ∧
    (∀s. P s ⇒ P (IMAGE g s)) ∧ (∀s t. s ⊆ IMAGE g t ⇔ IMAGE f s ⊆ t) ⇒
    P hull IMAGE f s = IMAGE f (P hull s)

⊢ ∀P f s.
    P (P hull s) ∧ (∀s. P s ⇒ P (IMAGE f s)) ⇒
    P hull IMAGE f s ⊆ IMAGE f (P hull s)

⊢ ∀P s x. x ∈ s ⇒ x ∈ P hull s

⊢ ∀P p s. (∀x. x ∈ s ⇒ p x) ∧ P {x | p x} ⇒ ∀x. x ∈ P hull s ⇒ p x

⊢ ∀P s t. s ⊆ t ∧ P t ⇒ P hull s ⊆ t

⊢ ∀P s t. s ⊆ t ⇒ P hull s ⊆ P hull t

⊢ ∀P s. P s ⇒ P hull s = s

⊢ ∀P Q.
    (∀f. (∀s. s ∈ f ⇒ P s) ⇒ P (BIGINTER f)) ∧
    (∀f. (∀s. s ∈ f ⇒ Q s) ⇒ Q (BIGINTER f)) ∧ (∀s. Q s ⇒ Q (P hull s)) ⇒
    (λx. P x ∧ Q x) hull s = P hull (Q hull s)

⊢ ∀P a s. a ∈ P hull s ⇒ P hull (a INSERT s) = P hull s

⊢ ∀P a s. a ∈ P hull s ⇔ P hull (a INSERT s) = P hull s

⊢ ∀P s. s ⊆ P hull s

⊢ ∀P s t. P hull s ∪ t = P hull (P hull s) ∪ (P hull t)

⊢ ∀P s t. P hull s ∪ t = P hull (P hull s) ∪ t

⊢ ∀P s t. P hull s ∪ t = P hull s ∪ (P hull t)

⊢ ∀P s t. (P hull s) ∪ (P hull t) ⊆ P hull s ∪ t

⊢ ∀P s t. s ⊆ t ∧ P t ∧ (∀t'. s ⊆ t' ∧ P t' ⇒ t ⊆ t') ⇒ P hull s = t

⊢ ∀p q r. p ∧ q ⇒ r ⇔ p ⇒ q ⇒ r

⊢ ∀t1 t2 t3. t1 ⇒ t2 ⇒ t3 ⇔ t1 ∧ t2 ⇒ t3

⊢ ∀top s t.
    closed_in top s ∧ top interior_of t = ∅ ⇒
    top interior_of (s ∪ t) = top interior_of s

⊢ ∀top s.
    top interior_of s =
    topspace top DIFF top closure_of (topspace top DIFF s)

⊢ ∀top s.
    top interior_of (topspace top DIFF s) =
    topspace top DIFF top closure_of s

⊢ ∀top. top interior_of ∅ = ∅

⊢ ∀top s. top interior_of s = s ⇔ open_in top s

⊢ ∀top s. top interior_of s = ∅ ⇔ ∀t. open_in top t ∧ t ⊆ s ⇒ t = ∅

⊢ ∀top s. top interior_of s = ∅ ⇔ ∀t. open_in top t ∧ t ≠ ∅ ⇒ t DIFF s ≠ ∅

⊢ ∀top s.
    top interior_of s = ∅ ⇔
    top closure_of (topspace top DIFF s) = topspace top

⊢ ∀top s t. top interior_of (s ∩ t) = top interior_of s ∩ top interior_of t

⊢ ∀top s. top interior_of top interior_of s = top interior_of s

⊢ ∀top f. top interior_of BIGINTER f ⊆ BIGINTER {top interior_of s | s ∈ f}

⊢ ∀top s t. t ⊆ s ∧ open_in top t ⇒ t ⊆ top interior_of s

⊢ ∀top s t. open_in top t ⇒ (t ⊆ top interior_of s ⇔ t ⊆ s)

⊢ ∀top s t. s ⊆ t ⇒ top interior_of s ⊆ top interior_of t

⊢ ∀top s. open_in top s ⇒ top interior_of s = s

⊢ ∀top s. top interior_of s = top interior_of (topspace top ∩ s)

⊢ ∀top s. top interior_of s ⊆ s

⊢ ∀top s. top interior_of s ⊆ top closure_of s

⊢ ∀top s t. subtopology top s interior_of t ⊆ s

⊢ ∀top s. top interior_of s ⊆ topspace top

⊢ ∀top s t u.
    s ⊆ t ∧ t ⊆ u ⇒
    subtopology top u interior_of s ⊆ subtopology top t interior_of s

⊢ ∀top u s.
    open_in top u ⇒ subtopology top u interior_of s = u ∩ top interior_of s

⊢ ∀top s u. u ∩ top interior_of s ⊆ subtopology top u interior_of s

⊢ ∀top s t u.
    t ⊆ u ⇒
    t ∩ subtopology top u interior_of s ⊆ subtopology top t interior_of s

⊢ ∀top. top interior_of topspace top = topspace top

⊢ ∀top s. BIGUNION {t | open_in top t ∧ t ⊆ s} = top interior_of s

⊢ ∀top s t.
    closed_in top s ∨ closed_in top t ⇒
    (top interior_of (s ∪ t) = ∅ ⇔
     top interior_of s = ∅ ∧ top interior_of t = ∅)

⊢ ∀top s. top interior_of s ∪ top frontier_of s = top closure_of s

⊢ ∀top s t.
    t ⊆ s ∧ open_in top t ∧ (∀t'. t' ⊆ s ∧ open_in top t' ⇒ t' ⊆ t) ⇒
    top interior_of s = t

⊢ ∀P Q. P ∅ ⇒ (P INTERSECTION_OF Q) 𝕌(:α)

⊢ ∀P Q s. P {s} ∧ Q s ⇒ (P INTERSECTION_OF Q) s

⊢ ∀P Q Q' s.
    (P INTERSECTION_OF Q) s ∧ (∀x. Q x ⇒ Q' x) ⇒ (P INTERSECTION_OF Q') s

⊢ BIGINTER ∅ = 𝕌(:α)

⊢ ∀P. BIGINTER {P} = P

⊢ ∀P Q. BIGINTER {P; Q} = P ∩ Q

⊢ (∀P f. BIGINTER {f x | P x} = {a | ∀x. P x ⇒ a ∈ f x}) ∧
  (∀P f. BIGINTER {f x y | P x y} = {a | ∀x y. P x y ⇒ a ∈ f x y}) ∧
  ∀P f. BIGINTER {f x y z | P x y z} = {a | ∀x y z. P x y z ⇒ a ∈ f x y z}

⊢ ∀f s. BIGINTER (IMAGE f s) = {y | ∀x. x ∈ s ⇒ y ∈ f x}

⊢ ∀P B. BIGINTER (P INSERT B) = P ∩ BIGINTER B

⊢ ∀u s. u ≠ ∅ ∧ (∀t. t ∈ u ⇒ t ⊆ s) ⇒ BIGINTER u ⊆ s

⊢ ∀u s. (∃t. t ∈ u ∧ t ⊆ s) ⇒ BIGINTER u ⊆ s

⊢ ∀s. BIGINTER s = 𝕌(:α) DIFF BIGUNION {𝕌(:α) DIFF t | t ∈ s}

⊢ (∀f s. s ∩ BIGINTER f = if f = ∅ then s else BIGINTER {s ∩ t | t ∈ f}) ∧
  ∀f s. BIGINTER f ∩ s = if f = ∅ then s else BIGINTER {t ∩ s | t ∈ f}

⊢ (∀s t. BIGUNION s ∩ t = BIGUNION {x ∩ t | x ∈ s}) ∧
  ∀s t. t ∩ BIGUNION s = BIGUNION {t ∩ x | x ∈ s}

⊢ ∀top s x.
    x ∈ top closure_of s ⇔
    x ∈ topspace top ∧ ∀t. x ∈ t ∧ open_in top t ⇒ ∃y. y ∈ s ∧ y ∈ t

⊢ ∀top s x.
    x ∈ top derived_set_of s ⇔
    x ∈ topspace top ∧
    ∀t. x ∈ t ∧ open_in top t ⇒ ∃y. y ≠ x ∧ y ∈ s ∧ y ∈ t

⊢ ∀s. {x | x ∈ s} = s

⊢ x ∈ BIGINTER B ⇔ ∀P. P ∈ B ⇒ x ∈ P

⊢ ∀x sos. x ∈ BIGUNION sos ⇔ ∃s. x ∈ s ∧ s ∈ sos

⊢ (∀s t. s ∈ B ∧ t ∈ B ⇒ s ∩ t ∈ B) ⇒ istopology (ARBITRARY UNION_OF B)

⊢ istopology (ARBITRARY UNION_OF P) ⇔
  ∀s t.
    s ∈ ARBITRARY UNION_OF P ∧ t ∈ ARBITRARY UNION_OF P ⇒
    s ∩ t ∈ ARBITRARY UNION_OF P

⊢ istopology (ARBITRARY UNION_OF P) ⇔
  ∀s t. s ∈ P ∧ t ∈ P ⇒ s ∩ t ∈ ARBITRARY UNION_OF P

⊢ ∀top. istopology (open_in top)

⊢ ∀top u. istopology {s ∩ u | open_in top s}

⊢ ∀P s. (∀f. (∀s. s ∈ f ⇒ P s) ⇒ P (BIGINTER f)) ⇒ (P s ⇔ ∃t. s = P hull t)

⊢ ∀P Q. (∃x. P x) ∧ Q ⇔ ∃x. P x ∧ Q

⊢ ∀top s.
    FINITE s ∧ s ≠ ∅ ∧ (∀t. t ∈ s ⇒ open_in top t) ⇒
    open_in top (BIGINTER s)

⊢ ∀top k. (∀s. s ∈ k ⇒ open_in top s) ⇒ open_in top (BIGUNION k)

⊢ ∀top.
    open_in top ∅ ∧
    (∀s t. open_in top s ∧ open_in top t ⇒ open_in top (s ∩ t)) ∧
    ∀k. (∀s. s ∈ k ⇒ open_in top s) ⇒ open_in top (BIGUNION k)

⊢ ∀top s.
    s ⊆ topspace top ⇒
    (open_in top s ⇔ closed_in top (topspace top DIFF s))

⊢ ∀top s.
    open_in top s ⇔ s ⊆ topspace top ∧ closed_in top (topspace top DIFF s)

⊢ ∀f top top' u.
    continuous_map (top,top') f ∧ open_in top' u ⇒
    open_in top {x | x ∈ topspace top ∧ f x ∈ u}

⊢ ∀f top top' u v.
    continuous_map (top,top') f ∧ open_in top u ∧ open_in top' v ⇒
    open_in top {x | x ∈ u ∧ f x ∈ v}

⊢ ∀top s t. open_in top s ∧ closed_in top t ⇒ open_in top (s DIFF t)

⊢ ∀top. open_in top ∅

⊢ ∀top s t. open_in (subtopology top s) t ⇒ t ⊆ s

⊢ ∀top s t. open_in top s ∧ open_in top t ⇒ open_in top (s ∩ t)

⊢ ∀top s. open_in top (top interior_of s)

⊢ ∀top s t.
    open_in top s ⇒ s ∩ top closure_of t = s ∩ top closure_of (s ∩ t)

⊢ ∀top s t. open_in top s ⇒ (s ∩ top closure_of t = ∅ ⇔ s ∩ t = ∅)

⊢ ∀top s t. open_in top s ⇒ s ∩ top closure_of t ⊆ top closure_of (s ∩ t)

⊢ ∀top s t.
    open_in top s ⇒
    s ∩ top derived_set_of t = s ∩ top derived_set_of (s ∩ t)

⊢ ∀top s t.
    open_in top s ⇒ s ∩ top derived_set_of t ⊆ top derived_set_of (s ∩ t)

⊢ ∀top s. open_in top relative_to s = open_in (subtopology top s)

⊢ ∀top s. open_in top s ⇔ ∀x. x ∈ s ⇒ ∃t. open_in top t ∧ x ∈ t ∧ t ⊆ s

⊢ ∀top s. open_in top s ⇒ s ⊆ topspace top

⊢ ∀top s. open_in top s ⇒ s ⊆ topspace top

⊢ ∀top u s. open_in (subtopology top u) s ⇔ ∃t. open_in top t ∧ s = t ∩ u

⊢ ∀top s. open_in (subtopology top ∅) s ⇔ s = ∅

⊢ ∀top u. open_in (subtopology top u) u ⇔ u ⊆ topspace top

⊢ ∀top s t u.
    open_in (subtopology top t) s ∧ open_in (subtopology top u) s ⇒
    open_in (subtopology top (t ∪ u)) s

⊢ open_in top = ARBITRARY UNION_OF B ⇔
  (∀v. v ∈ B ⇒ open_in top v) ∧
  ∀u x. open_in top u ∧ x ∈ u ⇒ ∃v. v ∈ B ∧ x ∈ v ∧ v ⊆ u

⊢ ∀top. open_in top (topspace top)

⊢ ∀top s t. open_in top s ∧ open_in top t ⇒ open_in top (s ∪ t)

⊢ ∀A top. open_in top A ⇔ ∀x. A x ⇒ ∃N. neigh top (N,x) ∧ N ⊆ A

⊢ ∀A top. open_in top A ⇔ ∀x. x ∈ A ⇒ ∃N. neigh top (N,x) ∧ N ⊆ A

⊢ ∀A top x. open_in top A ∧ A x ⇒ neigh top (A,x)

⊢ ∀S' top. open_in top S' ⇔ ∀x. S' x ⇒ ∃P. P x ∧ open_in top P ∧ P ⊆ S'

⊢ ∀S' top. open_in top S' ⇔ BIGUNION {P | open_in top P ∧ P ⊆ S'} = S'

⊢ ∀R R' s.
    pairwiseD R s ∧ pairwiseD R' s ⇔ pairwiseD (λx y. R x y ∧ R' x y) s

⊢ ∀r. pairwiseD r ∅ ⇔ T

⊢ ∀r f.
    pairwiseD r (IMAGE f s) ⇔ pairwiseD (λx y. f x ≠ f y ⇒ r (f x) (f y)) s

⊢ ∀P Q s.
    pairwiseD P s ∧ (∀x y. x ∈ s ∧ y ∈ s ∧ P x y ∧ x ≠ y ⇒ Q x y) ⇒
    pairwiseD Q s

⊢ ∀r x s.
    pairwiseD r (x INSERT s) ⇔
    (∀y. y ∈ s ∧ y ≠ x ⇒ r x y ∧ r y x) ∧ pairwiseD r s

⊢ ∀r s t. pairwiseD r s ∧ t ⊆ s ⇒ pairwiseD r t

⊢ ∀r x. pairwiseD r {x} ⇔ T

⊢ ∀R s t.
    pairwiseD R (s ∪ t) ⇔
    pairwiseD R s ∧ pairwiseD R t ∧
    ∀x y. x ∈ s DIFF t ∧ y ∈ t DIFF s ⇒ R x y ∧ R y x

⊢ ∀P s. (∀f. (∀s. s ∈ f ⇒ P s) ⇒ P (BIGINTER f)) ⇒ P (P hull s)

⊢ P relative_to u = {u ∩ s | P s}

⊢ ∀P u s.
    s ⊆ u ⇒
    ((P relative_to u) (u DIFF s) ⇔
     ((λc. P (𝕌(:α) DIFF c)) relative_to u) s)

⊢ ∀P s t. (P relative_to s) t ⇒ t ⊆ s

⊢ ∀P u s. P s ⇒ (P relative_to u) (u ∩ s)

⊢ ∀P s.
    (∀c d. P c ∧ P d ⇒ P (c ∩ d)) ⇒
    ∀c d.
      (P relative_to s) c ∧ (P relative_to s) d ⇒ (P relative_to s) (c ∩ d)

⊢ ∀P Q. (∀s. P s ⇒ Q s) ⇒ ∀u. (P relative_to u) s ⇒ (Q relative_to u) s

⊢ ∀P s t. P relative_to s relative_to t = P relative_to s ∩ t

⊢ ∀P s t. s ⊆ t ∧ P s ⇒ (P relative_to t) s

⊢ ∀P u s. s ⊆ u ∧ P s ⇒ (P relative_to u) s

⊢ ∀P u s t. (P relative_to u) s ∧ s ⊆ t ∧ t ⊆ u ⇒ (P relative_to t) s

⊢ ∀P s.
    (∀c d. P c ∧ P d ⇒ P (c ∪ d)) ⇒
    ∀c d.
      (P relative_to s) c ∧ (P relative_to s) d ⇒ (P relative_to s) (c ∪ d)

⊢ ∀P s. (P relative_to 𝕌(:α)) s ⇔ P s

⊢ ∀top top' f s.
    topspace top ⊆ s ⇒
    (continuous_map (top,top') (RESTRICTION s f) ⇔
     continuous_map (top,top') f)

⊢ ∀P Q. P ∧ (∃x. Q x) ⇔ ∃x. P ∧ Q x

⊢ ∀f s. {f x | x ∈ s} = IMAGE f s

⊢ (∀a. {x | x = a} = {a}) ∧ ∀a. {x | a = x} = {a}

⊢ ∀P s t. P t ⇒ (P hull s ⊆ t ⇔ s ⊆ t)

⊢ ∀f s t.
    s ⊆ IMAGE f t ⇔
    ∃u. u ⊆ t ∧ (∀x y. x ∈ u ∧ y ∈ u ⇒ (f x = f y ⇔ x = y)) ∧ s = IMAGE f u

⊢ ∀top s. s ⊆ top interior_of s ⇔ open_in top s

⊢ ∀s P. {x | x ∈ s ∧ P x} ⊆ s

⊢ ∀top s t. subtopology (subtopology top s) t = subtopology top (s ∩ t)

⊢ ∀top s. topspace top ⊆ s ⇒ subtopology top s = top

⊢ ∀top. subtopology top (topspace top) = top

⊢ ∀top. subtopology top 𝕌(:α) = top

⊢ (∀s. s ∈ P ⇒ open_in top s) ∧
  (∀u x. open_in top u ∧ x ∈ u ⇒ ∃b. b ∈ P ∧ x ∈ b ∧ b ⊆ u) ⇒
  topology (ARBITRARY UNION_OF P) = top

⊢ ∀top1 top2. top1 = top2 ⇔ ∀s. open_in top1 s ⇔ open_in top2 s

⊢ ∀top top'.
    topspace top' = topspace top ⇒
    ((∀s. open_in top s ⇒ open_in top' s) ⇔
     continuous_map (top',top) (λx. x))

⊢ ∀top u. topspace (subtopology top u) = topspace top ∩ u

⊢ BIGUNION ∅ = ∅

⊢ ∀x. BIGUNION {x} = x

⊢ ∀s t. BIGUNION {s; t} = s ∪ t

⊢ (∀P f. BIGUNION {f x | P x} = {a | ∃x. P x ∧ a ∈ f x}) ∧
  (∀P f. BIGUNION {f x y | P x y} = {a | ∃x y. P x y ∧ a ∈ f x y}) ∧
  ∀P f. BIGUNION {f x y z | P x y z} = {a | ∃x y z. P x y z ∧ a ∈ f x y z}

⊢ ∀f s. BIGUNION (IMAGE f s) = {y | ∃x. x ∈ s ∧ y ∈ f x}

⊢ ∀s P. BIGUNION (s INSERT P) = s ∪ BIGUNION P

⊢ ∀s. BIGUNION s = 𝕌(:α) DIFF BIGINTER {𝕌(:α) DIFF t | t ∈ s}

⊢ ∀X P. BIGUNION P ⊆ X ⇔ ∀Y. Y ∈ P ⇒ Y ⊆ X

⊢ ∀s1 s2. BIGUNION (s1 ∪ s2) = BIGUNION s1 ∪ BIGUNION s2

⊢ ∀top s t. top interior_of s ∪ top interior_of t ⊆ top interior_of (s ∪ t)

⊢ ∀P Q. P ∅ ⇒ (P UNION_OF Q) ∅

⊢ ∀P Q s. P {s} ∧ Q s ⇒ (P UNION_OF Q) s

⊢ ∀P Q Q' s. (P UNION_OF Q) s ∧ (∀x. Q x ⇒ Q' x) ⇒ (P UNION_OF Q') s

⊢ {x | T} = 𝕌(:α)

⊢ ∀top. closed top ⇒ topspace top = 𝕌(:α)

⊢ ∀top s. top derived_set_of s = {x | limpt top x s}

⊢ ∀top x s. limpt top x s ⇔ x ∈ top derived_set_of s

⊢ ∀top x s t. limpt top x s ∧ s ⊆ t ⇒ limpt top x t

⊢ ∀top x A.
    limpt top x A ⇔
    x ∈ topspace top ∧
    ∀U. open_in top U ∧ x ∈ U ⇒ ∃y. y ∈ U ∧ y ∈ A ∧ y ≠ x

⊢ ∀top N x.
    neigh top (N,x) ⇔ ∃P. open_in top P ∧ P ⊆ N ∧ x ∈ P ∧ N ⊆ topspace top

⊢ ∀top. open top ⇒ topspace top = 𝕌(:α)

⊢ ∀R. pairwiseD R = pairwiseN (RC R)