Theory: topology

Parents

• real

Types

• metric(Arity = 1)
• topology(Arity = 1)

Constants

• B  :'a metric -> 'a # real -> 'a -> bool
• istopology  :(('a -> bool) -> bool) -> bool
• re_subset  :('a -> bool) -> ('a -> bool) -> bool
• mr1  :real metric
• re_null  :'a -> bool
• ismet  :('a # 'a -> real) -> bool
• closed  :'a topology -> ('a -> bool) -> bool
• re_intersect  :('a -> bool) -> ('a -> bool) -> 'a -> bool
• dist  :'a metric -> 'a # 'a -> real
• limpt  :'a topology -> 'a -> ('a -> bool) -> bool
• re_compl  :('a -> bool) -> 'a -> bool
• topology  :(('a -> bool) -> bool) -> 'a topology
• neigh  :'a topology -> ('a -> bool) # 'a -> bool
• re_Union  :(('a -> bool) -> bool) -> 'a -> bool
• re_union  :('a -> bool) -> ('a -> bool) -> 'a -> bool
• metric  :('a # 'a -> real) -> 'a metric
• mtop  :'a metric -> 'a topology
• open  :'a topology -> ('a -> bool) -> bool
• re_universe  :'a -> bool

Definitions

ball

|- !m x e. B m (x,e) = (\y. dist m (x,y) < e)

closed

|- !L S'. closed L S' = open L (re_compl S')

ismet

|- !m.
     ismet m =
     (!x y. (m (x,y) = 0) = (x = y)) /\ !x y z. m (y,z) <= m (x,y) + m (x,z)

istopology

|- !L.
     istopology L =
     L re_null /\ L re_universe /\
     (!a b. L a /\ L b ==> L (a re_intersect b)) /\
     !P. P re_subset L ==> L (re_Union P)

limpt

|- !top x S'.
     limpt top x S' = !N. neigh top (N,x) ==> ?y. ~(x = y) /\ S' y /\ N y

metric_TY_DEF

|- ?rep. TYPE_DEFINITION ismet rep

metric_tybij

|- (!a. metric (dist a) = a) /\ !r. ismet r = (dist (metric r) = r)

mr1

|- mr1 = metric (\(x,y). abs (y - x))

mtop

|- !m.
     mtop m =
     topology (\S'. !x. S' x ==> ?e. 0 < e /\ !y. dist m (x,y) < e ==> S' y)

neigh

|- !top N x. neigh top (N,x) = ?P. open top P /\ P re_subset N /\ P x

re_compl

|- !P. re_compl P = (\x. ~P x)

re_intersect

|- !P Q. P re_intersect Q = (\x. P x /\ Q x)

re_null

|- re_null = (\x. F)

re_subset

|- !P Q. P re_subset Q = !x. P x ==> Q x

re_union

|- !P Q. P re_union Q = (\x. P x \/ Q x)

re_universe

|- re_universe = (\x. T)

topology_TY_DEF

|- ?rep. TYPE_DEFINITION istopology rep

topology_tybij

|- (!a. topology (open a) = a) /\ !r. istopology r = (open (topology r) = r)

Theorems

BALL_NEIGH

|- !m x e. 0 < e ==> neigh (mtop m) (B m (x,e),x)

BALL_OPEN

|- !m x e. 0 < e ==> open (mtop m) (B m (x,e))

CLOSED_LIMPT

|- !top S'. closed top S' = !x. limpt top x S' ==> S' x

COMPL_MEM

|- !P x. P x = ~re_compl P x

ISMET_R1

|- ismet (\(x,y). abs (y - x))

METRIC_ISMET

|- !m. ismet (dist m)

METRIC_NZ

|- !m x y. ~(x = y) ==> 0 < dist m (x,y)

METRIC_POS

|- !m x y. 0 <= dist m (x,y)

METRIC_SAME

|- !m x. dist m (x,x) = 0

METRIC_SYM

|- !m x y. dist m (x,y) = dist m (y,x)

METRIC_TRIANGLE

|- !m x y z. dist m (x,z) <= dist m (x,y) + dist m (y,z)

METRIC_ZERO

|- !m x y. (dist m (x,y) = 0) = (x = y)

MR1_ADD

|- !x d. dist mr1 (x,x + d) = abs d

MR1_ADD_LT

|- !x d. 0 < d ==> (dist mr1 (x,x + d) = d)

MR1_ADD_POS

|- !x d. 0 <= d ==> (dist mr1 (x,x + d) = d)

MR1_BETWEEN1

|- !x y z. x < z /\ dist mr1 (x,y) < z - x ==> y < z

MR1_DEF

|- !x y. dist mr1 (x,y) = abs (y - x)

MR1_LIMPT

|- !x. limpt (mtop mr1) x re_universe

MR1_SUB

|- !x d. dist mr1 (x,x - d) = abs d

MR1_SUB_LE

|- !x d. 0 <= d ==> (dist mr1 (x,x - d) = d)

MR1_SUB_LT

|- !x d. 0 < d ==> (dist mr1 (x,x - d) = d)

mtop_istopology

|- !m.
     istopology (\S'. !x. S' x ==> ?e. 0 < e /\ !y. dist m (x,y) < e ==> S' y)

MTOP_LIMPT

|- !m x S'.
     limpt (mtop m) x S' =
     !e. 0 < e ==> ?y. ~(x = y) /\ S' y /\ dist m (x,y) < e

MTOP_OPEN

|- !S' m.
     open (mtop m) S' =
     !x. S' x ==> ?e. 0 < e /\ !y. dist m (x,y) < e ==> S' y

OPEN_NEIGH

|- !S' top. open top S' = !x. S' x ==> ?N. neigh top (N,x) /\ N re_subset S'

OPEN_OWN_NEIGH

|- !S' top x. open top S' /\ S' x ==> neigh top (S',x)

OPEN_SUBOPEN

|- !S' top. open top S' = !x. S' x ==> ?P. P x /\ open top P /\ P re_subset S'

OPEN_UNOPEN

|- !S' top. open top S' = (re_Union (\P. open top P /\ P re_subset S') = S')

SUBSET_ANTISYM

|- !P Q. P re_subset Q /\ Q re_subset P = (P = Q)

SUBSET_REFL

|- !P. P re_subset P

SUBSET_TRANS

|- !P Q R. P re_subset Q /\ Q re_subset R ==> P re_subset R

TOPOLOGY

|- !L.
     open L re_null /\ open L re_universe /\
     (!x y. open L x /\ open L y ==> open L (x re_intersect y)) /\
     !P. P re_subset open L ==> open L (re_Union P)

TOPOLOGY_UNION

|- !L P. P re_subset open L ==> open L (re_Union P)