Theory "topology"

Parents quotient

Signature

Type	Arity
topology	1
Constant	Type
closed	:α topology -> bool
closed_in	:α topology -> (α -> bool) -> bool
hull	:((α -> bool) -> bool) -> (α -> bool) -> α -> bool
istopology	:((α -> bool) -> bool) -> bool
limpt	:α topology -> α -> (α -> bool) -> bool
neigh	:α topology -> (α -> bool) # α -> bool
open	:α topology -> bool
open_in	:α topology -> (α -> bool) -> bool
subtopology	:α topology -> (α -> bool) -> α topology
topology	:((α -> bool) -> bool) -> α topology
topspace	:α topology -> α -> bool

Definitions

closed_DEF

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

closed_in

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

hull

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

istopology

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

limpt

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

neigh

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

open_DEF

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

subtopology

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

topology_TY_DEF

⊢ ∃rep. TYPE_DEFINITION istopology rep

topology_tybij

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

topspace

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

Theorems

BIGINTER_2

⊢ ∀s t. BIGINTER {s; t} = s ∩ t

BIGUNION_2

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

CLOSED_IN_BIGINTER

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

CLOSED_IN_BIGUNION

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

CLOSED_IN_DIFF

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

CLOSED_IN_EMPTY

⊢ ∀top. closed_in top ∅

CLOSED_IN_IMP_SUBSET

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

CLOSED_IN_INTER

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

CLOSED_IN_OPEN_IN_COMPL

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

CLOSED_IN_SUBSET

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

CLOSED_IN_SUBTOPOLOGY

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

CLOSED_IN_SUBTOPOLOGY_EMPTY

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

CLOSED_IN_SUBTOPOLOGY_REFL

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

CLOSED_IN_SUBTOPOLOGY_UNION

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

CLOSED_IN_TOPSPACE

⊢ ∀top. closed_in top (topspace top)

CLOSED_IN_UNION

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

CLOSED_LIMPT

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

HULLS_EQ

⊢ ∀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)

HULL_ANTIMONO

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

HULL_EQ

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

HULL_HULL

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

HULL_IMAGE

⊢ ∀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))

HULL_IMAGE_GALOIS

⊢ ∀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))

HULL_IMAGE_SUBSET

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

HULL_INC

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

HULL_INDUCT

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

HULL_MINIMAL

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

HULL_MONO

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

HULL_P

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

HULL_P_AND_Q

⊢ ∀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))

HULL_REDUNDANT

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

HULL_REDUNDANT_EQ

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

HULL_SUBSET

⊢ ∀P s. s ⊆ P hull s

HULL_UNION

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

HULL_UNION_LEFT

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

HULL_UNION_RIGHT

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

HULL_UNION_SUBSET

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

HULL_UNIQUE

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

ISTOPOLOGY_OPEN_IN

⊢ ∀top. istopology (open_in top)

ISTOPOLOGY_SUBTOPOLOGY

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

IS_HULL

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

OPEN_IN_BIGINTER

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

OPEN_IN_BIGUNION

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

OPEN_IN_CLAUSES

⊢ ∀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)

OPEN_IN_CLOSED_IN

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

OPEN_IN_CLOSED_IN_EQ

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

OPEN_IN_DIFF

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

OPEN_IN_EMPTY

⊢ ∀top. open_in top ∅

OPEN_IN_IMP_SUBSET

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

OPEN_IN_INTER

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

OPEN_IN_SUBOPEN

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

OPEN_IN_SUBSET

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

OPEN_IN_SUBTOPOLOGY

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

OPEN_IN_SUBTOPOLOGY_EMPTY

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

OPEN_IN_SUBTOPOLOGY_REFL

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

OPEN_IN_SUBTOPOLOGY_UNION

⊢ ∀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_TOPSPACE

⊢ ∀top. open_in top (topspace top)

OPEN_IN_UNION

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

OPEN_NEIGH

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

OPEN_OWN_NEIGH

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

OPEN_SUBOPEN

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

OPEN_UNOPEN

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

P_HULL

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

SUBSET_HULL

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

SUBTOPOLOGY_SUPERSET

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

SUBTOPOLOGY_TOPSPACE

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

SUBTOPOLOGY_UNIV

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

TOPOLOGY_EQ

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

TOPSPACE_SUBTOPOLOGY

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

closed_topspace

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

open_topspace

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