|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"topology" > "topology_def"
|
|
|
7 |
"re_universe" > "re_universe_def"
|
|
|
8 |
"re_union" > "re_union_def"
|
|
|
9 |
"re_subset" > "re_subset_def"
|
|
|
10 |
"re_null" > "re_null_def"
|
|
|
11 |
"re_intersect" > "re_intersect_def"
|
|
|
12 |
"re_compl" > "re_compl_def"
|
|
|
13 |
"re_Union" > "re_Union_def"
|
|
|
14 |
"open" > "open_def"
|
|
|
15 |
"neigh" > "neigh_def"
|
|
|
16 |
"mtop" > "mtop_def"
|
|
|
17 |
"mr1" > "mr1_def"
|
|
|
18 |
"metric" > "metric_def"
|
|
|
19 |
"limpt" > "limpt_def"
|
|
|
20 |
"istopology" > "istopology_def"
|
|
|
21 |
"ismet" > "ismet_def"
|
|
|
22 |
"dist" > "dist_def"
|
|
|
23 |
"closed" > "closed_def"
|
|
|
24 |
"B" > "B_def"
|
|
|
25 |
|
|
|
26 |
type_maps
|
|
|
27 |
"topology" > "HOL4Real.topology.topology"
|
|
|
28 |
"metric" > "HOL4Real.topology.metric"
|
|
|
29 |
|
|
|
30 |
const_maps
|
|
|
31 |
"re_universe" > "HOL4Real.topology.re_universe"
|
|
|
32 |
"re_union" > "HOL4Real.topology.re_union"
|
|
|
33 |
"re_subset" > "HOL4Real.topology.re_subset"
|
|
|
34 |
"re_null" > "HOL4Real.topology.re_null"
|
|
|
35 |
"re_intersect" > "HOL4Real.topology.re_intersect"
|
|
|
36 |
"re_compl" > "HOL4Real.topology.re_compl"
|
|
|
37 |
"re_Union" > "HOL4Real.topology.re_Union"
|
|
|
38 |
"neigh" > "HOL4Real.topology.neigh"
|
|
|
39 |
"mtop" > "HOL4Real.topology.mtop"
|
|
|
40 |
"mr1" > "HOL4Real.topology.mr1"
|
|
|
41 |
"limpt" > "HOL4Real.topology.limpt"
|
|
|
42 |
"istopology" > "HOL4Real.topology.istopology"
|
|
|
43 |
"ismet" > "HOL4Real.topology.ismet"
|
|
|
44 |
"closed" > "HOL4Real.topology.closed"
|
|
|
45 |
"B" > "HOL4Real.topology.B"
|
|
|
46 |
|
|
|
47 |
thm_maps
|
|
|
48 |
"topology_tybij" > "HOL4Real.topology.topology_tybij"
|
|
|
49 |
"topology_TY_DEF" > "HOL4Real.topology.topology_TY_DEF"
|
|
|
50 |
"re_universe_def" > "HOL4Real.topology.re_universe_def"
|
|
|
51 |
"re_universe" > "HOL4Real.topology.re_universe"
|
|
|
52 |
"re_union_def" > "HOL4Real.topology.re_union_def"
|
|
|
53 |
"re_union" > "HOL4Real.topology.re_union"
|
|
|
54 |
"re_subset_def" > "HOL4Real.topology.re_subset_def"
|
|
|
55 |
"re_subset" > "HOL4Real.topology.re_subset"
|
|
|
56 |
"re_null_def" > "HOL4Real.topology.re_null_def"
|
|
|
57 |
"re_null" > "HOL4Real.topology.re_null"
|
|
|
58 |
"re_intersect_def" > "HOL4Real.topology.re_intersect_def"
|
|
|
59 |
"re_intersect" > "HOL4Real.topology.re_intersect"
|
|
|
60 |
"re_compl_def" > "HOL4Real.topology.re_compl_def"
|
|
|
61 |
"re_compl" > "HOL4Real.topology.re_compl"
|
|
|
62 |
"re_Union_def" > "HOL4Real.topology.re_Union_def"
|
|
|
63 |
"re_Union" > "HOL4Real.topology.re_Union"
|
|
|
64 |
"neigh_def" > "HOL4Real.topology.neigh_def"
|
|
|
65 |
"neigh" > "HOL4Real.topology.neigh"
|
|
|
66 |
"mtop_istopology" > "HOL4Real.topology.mtop_istopology"
|
|
|
67 |
"mtop_def" > "HOL4Real.topology.mtop_def"
|
|
|
68 |
"mtop" > "HOL4Real.topology.mtop"
|
|
|
69 |
"mr1_def" > "HOL4Real.topology.mr1_def"
|
|
|
70 |
"mr1" > "HOL4Real.topology.mr1"
|
|
|
71 |
"metric_tybij" > "HOL4Real.topology.metric_tybij"
|
|
|
72 |
"metric_TY_DEF" > "HOL4Real.topology.metric_TY_DEF"
|
|
|
73 |
"limpt_def" > "HOL4Real.topology.limpt_def"
|
|
|
74 |
"limpt" > "HOL4Real.topology.limpt"
|
|
|
75 |
"istopology_def" > "HOL4Real.topology.istopology_def"
|
|
|
76 |
"istopology" > "HOL4Real.topology.istopology"
|
|
|
77 |
"ismet_def" > "HOL4Real.topology.ismet_def"
|
|
|
78 |
"ismet" > "HOL4Real.topology.ismet"
|
|
|
79 |
"closed_def" > "HOL4Real.topology.closed_def"
|
|
|
80 |
"closed" > "HOL4Real.topology.closed"
|
|
|
81 |
"ball" > "HOL4Real.topology.ball"
|
|
|
82 |
"TOPOLOGY_UNION" > "HOL4Real.topology.TOPOLOGY_UNION"
|
|
|
83 |
"TOPOLOGY" > "HOL4Real.topology.TOPOLOGY"
|
|
|
84 |
"SUBSET_TRANS" > "HOL4Real.topology.SUBSET_TRANS"
|
|
|
85 |
"SUBSET_REFL" > "HOL4Real.topology.SUBSET_REFL"
|
|
|
86 |
"SUBSET_ANTISYM" > "HOL4Real.topology.SUBSET_ANTISYM"
|
|
|
87 |
"OPEN_UNOPEN" > "HOL4Real.topology.OPEN_UNOPEN"
|
|
|
88 |
"OPEN_SUBOPEN" > "HOL4Real.topology.OPEN_SUBOPEN"
|
|
|
89 |
"OPEN_OWN_NEIGH" > "HOL4Real.topology.OPEN_OWN_NEIGH"
|
|
|
90 |
"OPEN_NEIGH" > "HOL4Real.topology.OPEN_NEIGH"
|
|
|
91 |
"MTOP_OPEN" > "HOL4Real.topology.MTOP_OPEN"
|
|
|
92 |
"MTOP_LIMPT" > "HOL4Real.topology.MTOP_LIMPT"
|
|
|
93 |
"MR1_SUB_LT" > "HOL4Real.topology.MR1_SUB_LT"
|
|
|
94 |
"MR1_SUB_LE" > "HOL4Real.topology.MR1_SUB_LE"
|
|
|
95 |
"MR1_SUB" > "HOL4Real.topology.MR1_SUB"
|
|
|
96 |
"MR1_LIMPT" > "HOL4Real.topology.MR1_LIMPT"
|
|
|
97 |
"MR1_DEF" > "HOL4Real.topology.MR1_DEF"
|
|
|
98 |
"MR1_BETWEEN1" > "HOL4Real.topology.MR1_BETWEEN1"
|
|
|
99 |
"MR1_ADD_POS" > "HOL4Real.topology.MR1_ADD_POS"
|
|
|
100 |
"MR1_ADD_LT" > "HOL4Real.topology.MR1_ADD_LT"
|
|
|
101 |
"MR1_ADD" > "HOL4Real.topology.MR1_ADD"
|
|
|
102 |
"METRIC_ZERO" > "HOL4Real.topology.METRIC_ZERO"
|
|
|
103 |
"METRIC_TRIANGLE" > "HOL4Real.topology.METRIC_TRIANGLE"
|
|
|
104 |
"METRIC_SYM" > "HOL4Real.topology.METRIC_SYM"
|
|
|
105 |
"METRIC_SAME" > "HOL4Real.topology.METRIC_SAME"
|
|
|
106 |
"METRIC_POS" > "HOL4Real.topology.METRIC_POS"
|
|
|
107 |
"METRIC_NZ" > "HOL4Real.topology.METRIC_NZ"
|
|
|
108 |
"METRIC_ISMET" > "HOL4Real.topology.METRIC_ISMET"
|
|
|
109 |
"ISMET_R1" > "HOL4Real.topology.ISMET_R1"
|
|
|
110 |
"COMPL_MEM" > "HOL4Real.topology.COMPL_MEM"
|
|
|
111 |
"CLOSED_LIMPT" > "HOL4Real.topology.CLOSED_LIMPT"
|
|
|
112 |
"B_def" > "HOL4Real.topology.B_def"
|
|
|
113 |
"BALL_OPEN" > "HOL4Real.topology.BALL_OPEN"
|
|
|
114 |
"BALL_NEIGH" > "HOL4Real.topology.BALL_NEIGH"
|
|
|
115 |
|
|
|
116 |
end
|