Skip to content

Commit

Permalink
Added quite a few theorems, all fairly straightforward and many in
Browse files Browse the repository at this point in the history 
the "general topology" area, some being natural generalizations of
existing Euclidean ones. New theorems:

        ALWAYS_WITHIN_EVENTUALLY
        ARCH_EVENTUALLY_ABS_INV_OFFSET
        ARCH_EVENTUALLY_INV_OFFSET
        CAUCHY_IN_CONVERGENT_SUBSEQUENCE
        CAUCHY_IN_INTERLEAVING_GEN
        CAUCHY_IN_OFFSET
        CAUCHY_IN_SUBSEQUENCE
        CLOSED_IN_TRANS_FULL
        CLOSURE_OF_SEQUENTIALLY
        CONTINUOUS_MAP_FROM_SUBTOPOLOGY_MONO
        CONTINUOUS_MAP_MDIST_ALT
        CROSS_SING
        DERIVED_SET_OF_SEQUENTIALLY
        DERIVED_SET_OF_SEQUENTIALLY_ALT
        DERIVED_SET_OF_SEQUENTIALLY_DECREASING
        DERIVED_SET_OF_SEQUENTIALLY_DECREASING_ALT
        DERIVED_SET_OF_SEQUENTIALLY_INJ
        DERIVED_SET_OF_SEQUENTIALLY_INJ_ALT
        DERIVED_SET_OF_TRIVIAL_LIMIT
        EVENTUALLY_ATPOINTOF_SEQUENTIALLY
        EVENTUALLY_ATPOINTOF_SEQUENTIALLY_DECREASING
        EVENTUALLY_ATPOINTOF_SEQUENTIALLY_INJ
        EVENTUALLY_ATPOINTOF_WITHIN_SEQUENTIALLY
        EVENTUALLY_ATPOINTOF_WITHIN_SEQUENTIALLY_DECREASING
        EVENTUALLY_ATPOINTOF_WITHIN_SEQUENTIALLY_INJ
        EVENTUALLY_WITHIN_SUBSET
        EXISTS_CLOSED_IN
        EXISTS_OPEN_IN
        EXISTS_PAIR_FUN_THM
        FORALL_CLOSED_IN
        FORALL_OPEN_IN
        FORALL_PAIR_FUN_THM
        HAUSDORFF_SPACE_INJECTIVE_PREIMAGE
        IN_INTERIOR_OF_MBALL
        IN_INTERIOR_OF_MCBALL
        LIMIT_ATPOINTOF_SELF
        LIMIT_ATPOINTOF_SEQUENTIALLY
        LIMIT_ATPOINTOF_SEQUENTIALLY_DECREASING
        LIMIT_ATPOINTOF_SEQUENTIALLY_INJ
        LIMIT_ATPOINTOF_SEQUENTIALLY_WITHIN
        LIMIT_ATPOINTOF_SEQUENTIALLY_WITHIN_DECREASING
        LIMIT_ATPOINTOF_SEQUENTIALLY_WITHIN_INJ
        LIMIT_EVENTUALLY
        LIMIT_METRIC_DIST_NULL
        LIMIT_SUBSEQUENCE
        LIMIT_TRANSFORM_EVENTUALLY
        LIMIT_WITHIN_SUBSET
        MBOUNDED_ALT
        MBOUNDED_ALT_POS
        MBOUNDED_POS
        MBOUNDED_REAL_EUCLIDEAN_METRIC
        MCOMPLETE_DISCRETE_METRIC
        METRIC_CLOSURE_OF_ALT
        METRIC_INTERIOR_OF
        METRIC_INTERIOR_OF_ALT
        OPEN_IN_TRANS_FULL
        PCROSS_SING
        PROD_TOPOLOGY_DISCRETE_TOPOLOGY
        REGULAR_CLOSED
        REGULAR_CLOSED_IN
        REGULAR_CLOSURE_IMP_THIN_FRONTIER
        REGULAR_CLOSURE_INTERIOR
        REGULAR_CLOSURE_OF_IMP_THIN_FRONTIER_OF
        REGULAR_CLOSURE_OF_INTERIOR_OF
        REGULAR_INTERIOR_CLOSURE
        REGULAR_INTERIOR_IMP_THIN_FRONTIER
        REGULAR_INTERIOR_OF_CLOSURE_OF
        REGULAR_INTERIOR_OF_IMP_THIN_FRONTIER_OF
        REGULAR_OPEN
        REGULAR_OPEN_IN
        SUBMETRIC_MSPACE
        SUBMETRIC_RESTRICT
        SUBMETRIC_SUBMETRIC
        TOTALLY_BOUNDED_IN_CAUCHY_SEQUENCE

Also renamed two existing theorems:

      CLOSURE_IN_CROSS -> CLOSURE_OF_CROSS
      INTERIOR_IN_CROSS -> INTERIOR_OF_CROSS
  • Loading branch information
@jrh13
jrh13 committed Apr 17, 2017
1 parent 2430ee0 commit 2ef4029
Show file tree
Hide file tree
Showing 10 changed files with 1,155 additions and 162 deletions.
16 changes: 16 additions & 0 deletions CHANGES
View file
Expand Up @@ -8,6 +8,22 @@
* page: https://github.com/jrh13/hol-light/commits/master *
* *****************************************************************

Wed 11th Apr 2017 pair.ml, sets.ml, cart.ml

Added a few more trivial but nice-to-have rewrites:

EXISTS_PAIR_FUN_THM =
|- !P. (?f. P f) <=> (?g h. P (\a. g a,h a))

FORALL_PAIR_FUN_THM =
|- !P. (!f. P f) <=> (!g h. P (\a. g a,h a))

CROSS_SING =
|- !x y. {x} CROSS {y} = {(x,y)}

PCROSS_SING =
|- !x y. {x} PCROSS {y} = {pastecart x y}

Sat 8th Apr 2017 cart.ml

Type-generalized PASTECART_INJ which had a pointless restriction to ":real".
Expand Down
78 changes: 76 additions & 2 deletions Multivariate/complex_database.ml
View file

Large diffs are not rendered by default.

972 changes: 897 additions & 75 deletions Multivariate/metric.ml
View file

Large diffs are not rendered by default.

80 changes: 78 additions & 2 deletions Multivariate/multivariate_database.ml
View file

Large diffs are not rendered by default.

8 changes: 0 additions & 8 deletions Multivariate/realanalysis.ml
View file
Expand Up @@ -29,18 +29,10 @@ let REAL_CLOSED = prove
(* Compactness of a set of reals. *)
(* ------------------------------------------------------------------------- *)

let real_bounded = new_definition
`real_bounded s <=> ?B. !x. x IN s ==> abs(x) <= B`;;

let REAL_BOUNDED = prove
(`real_bounded s <=> bounded(IMAGE lift s)`,
REWRITE_TAC[BOUNDED_LIFT; real_bounded]);;

let REAL_BOUNDED_POS = prove
(`!s. real_bounded s <=> ?B. &0 < B /\ !x. x IN s ==> abs(x) <= B`,
REWRITE_TAC[real_bounded] THEN
MESON_TAC[REAL_ARITH `&0 < &1 + abs B /\ (x <= B ==> x <= &1 + abs B)`]);;

let REAL_BOUNDED_POS_LT = prove
(`!s. real_bounded s <=> ?b. &0 < b /\ !x. x IN s ==> abs(x) < b`,
REWRITE_TAC[real_bounded] THEN
Expand Down
139 changes: 64 additions & 75 deletions Multivariate/topology.ml
View file
Expand Up @@ -2527,6 +2527,44 @@ let FRONTIER_FRONTIER_FRONTIER = prove
(`!s:real^N->bool. frontier(frontier(frontier s)) = frontier(frontier s)`,
SIMP_TAC[FRONTIER_FRONTIER; FRONTIER_CLOSED]);;

let REGULAR_CLOSURE_INTERIOR = prove
(`!s:real^N->bool.
s SUBSET closure(interior s) <=>
closure(interior s) = closure s`,
REWRITE_TAC[GSYM EUCLIDEAN_CLOSURE_OF; GSYM EUCLIDEAN_INTERIOR_OF] THEN
SIMP_TAC[REGULAR_CLOSURE_OF_INTERIOR_OF; TOPSPACE_EUCLIDEAN; SUBSET_UNIV]);;

let REGULAR_INTERIOR_CLOSURE = prove
(`!s:real^N->bool.
interior(closure s) SUBSET s <=>
interior(closure s) = interior s`,
REWRITE_TAC[GSYM EUCLIDEAN_CLOSURE_OF; GSYM EUCLIDEAN_INTERIOR_OF] THEN
REWRITE_TAC[REGULAR_INTERIOR_OF_CLOSURE_OF]);;

let REGULAR_CLOSED = prove
(`!s:real^N->bool.
closure(interior s) = s <=>
closed s /\ s SUBSET closure(interior s)`,
REWRITE_TAC[GSYM EUCLIDEAN_CLOSURE_OF; GSYM EUCLIDEAN_INTERIOR_OF] THEN
REWRITE_TAC[CLOSED_IN; REGULAR_CLOSED_IN]);;

let REGULAR_OPEN = prove
(`!s:real^N->bool.
interior(closure s) = s <=>
open s /\ interior(closure s) SUBSET s`,
REWRITE_TAC[GSYM EUCLIDEAN_CLOSURE_OF; GSYM EUCLIDEAN_INTERIOR_OF] THEN
REWRITE_TAC[OPEN_IN; REGULAR_OPEN_IN]);;

let REGULAR_CLOSURE_IMP_THIN_FRONTIER = prove
(`!s:real^N->bool.
s SUBSET closure(interior s) ==> interior(frontier s) = {}`,
SIMP_TAC[REGULAR_CLOSURE_INTERIOR; THIN_FRONTIER_ICI]);;

let REGULAR_INTERIOR_IMP_THIN_FRONTIER = prove
(`!s:real^N->bool.
interior(closure s) SUBSET s ==> interior(frontier s) = {}`,
SIMP_TAC[REGULAR_INTERIOR_CLOSURE; THIN_FRONTIER_CIC]);;

let UNION_FRONTIER = prove
(`!s t:real^N->bool.
frontier(s) UNION frontier(t) =
Expand Down Expand Up @@ -5506,14 +5544,6 @@ let CAUCHY_OFFSET = prove
MESON_TAC[ARITH_RULE
`N + k:num <= n ==> n = (n - k) + k /\ N <= n - k`]);;

let CONVERGENT_IMP_CAUCHY = prove
(`!s l. (s --> l) sequentially ==> cauchy s`,
REWRITE_TAC[LIM_SEQUENTIALLY; cauchy] THEN
REPEAT GEN_TAC THEN DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `e / &2`) THEN
ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
ASM_MESON_TAC[GE; LE_REFL; DIST_TRIANGLE_HALF_L]);;

let CONVERGENT_IMP_CAUCHY = prove
(`!s l. (s --> l) sequentially ==> cauchy s`,
REWRITE_TAC[GSYM LIMIT_EUCLIDEAN; GSYM CAUCHY_IN_EUCLIDEAN] THEN
Expand Down Expand Up @@ -6728,80 +6758,43 @@ let UNIFORMLY_CONTINUOUS_ON_SEQUENTIALLY,
REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN
ASM_ARITH_TAC]);;

let [LIM_WITHIN_SEQUENTIALLY;
LIM_WITHIN_SEQUENTIALLY_INJ;
LIM_WITHIN_SEQUENTIALLY_DECREASING] = (CONJUNCTS o prove)
(`(!f:real^M->real^N s a l.
let LIM_WITHIN_SEQUENTIALLY = prove
(`!f:real^M->real^N s a l.
(f --> l) (at a within s) <=>
!x. (!n. x(n) IN s DELETE a) /\
(x --> a) sequentially
==> ((f o x) --> l) sequentially) /\
(!f:real^M->real^N s a l.
==> ((f o x) --> l) sequentially`,
REPEAT GEN_TAC THEN REWRITE_TAC[GSYM LIMIT_EUCLIDEAN; at] THEN
REWRITE_TAC[GSYM MTOPOLOGY_EUCLIDEAN_METRIC] THEN
GEN_REWRITE_TAC LAND_CONV [LIMIT_ATPOINTOF_SEQUENTIALLY_WITHIN] THEN
REWRITE_TAC[EUCLIDEAN_METRIC; IN_UNIV; INTER_UNIV]);;

let LIM_WITHIN_SEQUENTIALLY_INJ = prove
(`!f:real^M->real^N s a l.
(f --> l) (at a within s) <=>
!x. (!n. x(n) IN s DELETE a) /\
(!m n. x m = x n <=> m = n) /\
(x --> a) sequentially
==> ((f o x) --> l) sequentially) /\
(!f:real^M->real^N s a l.
==> ((f o x) --> l) sequentially`,
REPEAT GEN_TAC THEN REWRITE_TAC[GSYM LIMIT_EUCLIDEAN; at] THEN
REWRITE_TAC[GSYM MTOPOLOGY_EUCLIDEAN_METRIC] THEN
GEN_REWRITE_TAC LAND_CONV [LIMIT_ATPOINTOF_SEQUENTIALLY_WITHIN_INJ] THEN
REWRITE_TAC[EUCLIDEAN_METRIC; IN_UNIV; INTER_UNIV]);;

let LIM_WITHIN_SEQUENTIALLY_DECREASING = prove
(`!f:real^M->real^N s a l.
(f --> l) (at a within s) <=>
!x. (!n. x(n) IN s DELETE a) /\
(!m n. m < n ==> dist(x n,a) < dist(x m,a)) /\
(x --> a) sequentially
==> ((f o x) --> l) sequentially)`,
REWRITE_TAC[AND_FORALL_THM] THEN REPEAT GEN_TAC THEN
MATCH_MP_TAC(TAUT
`(r ==> s) /\ (q ==> r) /\ (p ==> q) /\ (s ==> p)
==> (p <=> q) /\ (p <=> r) /\ (p <=> s)`) THEN
REPEAT CONJ_TAC THENL
[MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `x:num->real^M` THEN
DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN MATCH_MP_TAC THEN
MATCH_MP_TAC WLOG_LT THEN REWRITE_TAC[] THEN
ASM_MESON_TAC[REAL_LT_REFL];
MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `x:num->real^M` THEN
MESON_TAC[];
SIMP_TAC[LIM_WITHIN; LIM_SEQUENTIALLY; GSYM DIST_NZ; o_THM; IN_DELETE] THEN
MESON_TAC[];
DISCH_TAC THEN REWRITE_TAC[LIM_WITHIN] THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN
PURE_REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(p /\ q) <=> p ==> ~q`;
NOT_FORALL_THM; NOT_IMP; GSYM CONJ_ASSOC; REAL_NOT_LT] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (MESON[]
`(!x. P x ==> Q x) ==> (R ==> (?x. P x /\ ~Q x)) ==> R ==> F`)) THEN
DISCH_TAC THEN
SUBGOAL_THEN
`?x. (!n. (x n) IN s /\ ~(x n = a) /\
e <= dist((f:real^M->real^N)(x n),l) /\
dist(x n,a) < inv(&n + &1)) /\
(!n. dist(x(SUC n),a) < dist(x n,a))`
MP_TAC THENL
[MATCH_MP_TAC DEPENDENT_CHOICE THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
CONJ_TAC THENL [ASM_MESON_TAC[REAL_LT_01; DIST_NZ]; ALL_TAC] THEN
MAP_EVERY X_GEN_TAC [`n:num`; `x:real^M`] THEN
STRIP_TAC THEN REWRITE_TAC[GSYM CONJ_ASSOC; GSYM REAL_LT_MIN] THEN
REWRITE_TAC[DIST_NZ] THEN
ONCE_REWRITE_TAC[TAUT `p /\ q /\ r /\ s <=> p /\ q /\ s /\ r`] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
ASM_REWRITE_TAC[REAL_LT_MIN; REAL_LT_INV_EQ; GSYM DIST_NZ] THEN
REAL_ARITH_TAC;
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `x:num->real^M` THEN
REWRITE_TAC[FORALL_AND_THM] THEN STRIP_TAC THEN
ASM_REWRITE_TAC[IN_DELETE] THEN REPEAT CONJ_TAC THENL
[MATCH_MP_TAC TRANSITIVE_STEPWISE_LT THEN
ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
REWRITE_TAC[LIM_SEQUENTIALLY] THEN MATCH_MP_TAC FORALL_POS_MONO_1 THEN
CONJ_TAC THENL [MESON_TAC[REAL_LT_TRANS]; ALL_TAC] THEN
X_GEN_TAC `N:num` THEN EXISTS_TAC `N:num` THEN
X_GEN_TAC `n:num` THEN DISCH_TAC THEN
TRANS_TAC REAL_LTE_TRANS `inv(&n + &1)` THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
REWRITE_TAC[REAL_OF_NUM_LE; REAL_OF_NUM_LT; REAL_OF_NUM_ADD] THEN
ASM_ARITH_TAC;
REWRITE_TAC[LIM_SEQUENTIALLY; NOT_FORALL_THM] THEN
EXISTS_TAC `e:real` THEN ASM_REWRITE_TAC[NOT_EXISTS_THM] THEN
ASM_REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; REAL_NOT_LT; o_DEF] THEN
MESON_TAC[LE_REFL]]]]);;
==> ((f o x) --> l) sequentially`,
REPEAT GEN_TAC THEN REWRITE_TAC[GSYM LIMIT_EUCLIDEAN; at] THEN
REWRITE_TAC[GSYM MTOPOLOGY_EUCLIDEAN_METRIC] THEN GEN_REWRITE_TAC LAND_CONV
[LIMIT_ATPOINTOF_SEQUENTIALLY_WITHIN_DECREASING] THEN
REWRITE_TAC[EUCLIDEAN_METRIC; IN_UNIV; INTER_UNIV] THEN
EQ_TAC THEN MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN
REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC WLOG_LT THEN ASM_MESON_TAC[REAL_LT_REFL]);;

let LIM_AT_SEQUENTIALLY = prove
(`!f:real^M->real^N a l.
Expand Down Expand Up @@ -14030,10 +14023,6 @@ let NOT_INTERVAL_UNIV = prove
(!a b. ~(interval(a,b) = UNIV))`,
MESON_TAC[BOUNDED_INTERVAL; NOT_BOUNDED_UNIV]);;

let COMPACT_INTERVAL = prove
(`!a b. compact (interval [a,b])`,
SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED; BOUNDED_INTERVAL; CLOSED_INTERVAL]);;

let OPEN_INTERVAL_MIDPOINT = prove
(`!a b:real^N.
~(interval(a,b) = {}) ==> (inv(&2) % (a + b)) IN interval(a,b)`,
Expand Down
5 changes: 5 additions & 0 deletions cart.ml
View file
Expand Up @@ -459,6 +459,11 @@ let PCROSS_EMPTY = prove
(`(!s. s PCROSS {} = {}) /\ (!t. {} PCROSS t = {})`,
REWRITE_TAC[PCROSS_EQ_EMPTY]);;

let PCROSS_SING = prove
(`!x y:A^N. {x} PCROSS {y} = {pastecart x y}`,
REWRITE_TAC[EXTENSION; FORALL_PASTECART; IN_SING; PASTECART_IN_PCROSS;
PASTECART_INJ]);;

let SUBSET_PCROSS = prove
(`!s t s' t'. s PCROSS t SUBSET s' PCROSS t' <=>
s = {} \/ t = {} \/ s SUBSET s' /\ t SUBSET t'`,
Expand Down
4 changes: 4 additions & 0 deletions database.ml
View file
Expand Up @@ -211,6 +211,7 @@ theorems :=
"CROSS_INTERS",CROSS_INTERS;
"CROSS_INTERS_INTERS",CROSS_INTERS_INTERS;
"CROSS_MONO",CROSS_MONO;
"CROSS_SING",CROSS_SING;
"CROSS_UNION",CROSS_UNION;
"CROSS_UNIONS",CROSS_UNIONS;
"CROSS_UNIONS_UNIONS",CROSS_UNIONS_UNIONS;
Expand Down Expand Up @@ -380,6 +381,7 @@ theorems :=
"EXISTS_ONE_REP",EXISTS_ONE_REP;
"EXISTS_OR_THM",EXISTS_OR_THM;
"EXISTS_PAIRED_THM",EXISTS_PAIRED_THM;
"EXISTS_PAIR_FUN_THM",EXISTS_PAIR_FUN_THM;
"EXISTS_PAIR_THM",EXISTS_PAIR_THM;
"EXISTS_PASTECART",EXISTS_PASTECART;
"EXISTS_REFL",EXISTS_REFL;
Expand Down Expand Up @@ -541,6 +543,7 @@ theorems :=
"FORALL_IN_UNIONS",FORALL_IN_UNIONS;
"FORALL_NOT_THM",FORALL_NOT_THM;
"FORALL_PAIRED_THM",FORALL_PAIRED_THM;
"FORALL_PAIR_FUN_THM",FORALL_PAIR_FUN_THM;
"FORALL_PAIR_THM",FORALL_PAIR_THM;
"FORALL_PASTECART",FORALL_PASTECART;
"FORALL_SIMP",FORALL_SIMP;
Expand Down Expand Up @@ -1545,6 +1548,7 @@ theorems :=
"PCROSS_INTERS",PCROSS_INTERS;
"PCROSS_INTERS_INTERS",PCROSS_INTERS_INTERS;
"PCROSS_MONO",PCROSS_MONO;
"PCROSS_SING",PCROSS_SING;
"PCROSS_UNION",PCROSS_UNION;
"PCROSS_UNIONS",PCROSS_UNIONS;
"PCROSS_UNIONS_UNIONS",PCROSS_UNIONS_UNIONS;
Expand Down
11 changes: 11 additions & 0 deletions pair.ml
View file
Expand Up @@ -341,6 +341,17 @@ let EXISTS_UNPAIR_THM = prove
(`!P. (?x y. P x y) <=> ?z. P (FST z) (SND z)`,
REWRITE_TAC[EXISTS_PAIR_THM; FST; SND] THEN MESON_TAC[]);;

let FORALL_PAIR_FUN_THM = prove
(`!P. (!f:A->B#C. P f) <=> (!g h. P(\a. g a,h a))`,
GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
GEN_TAC THEN GEN_REWRITE_TAC RAND_CONV [GSYM ETA_AX] THEN
GEN_REWRITE_TAC BINDER_CONV [GSYM PAIR] THEN PURE_ASM_REWRITE_TAC[]);;

let EXISTS_PAIR_FUN_THM = prove
(`!P. (?f:A->B#C. P f) <=> (?g h. P(\a. g a,h a))`,
REWRITE_TAC[MESON[] `(?x. P x) <=> ~(!x. ~P x)`] THEN
REWRITE_TAC[FORALL_PAIR_FUN_THM]);;

(* ------------------------------------------------------------------------- *)
(* Related theorems for explicitly paired quantifiers. *)
(* ------------------------------------------------------------------------- *)
Expand Down
4 changes: 4 additions & 0 deletions sets.ml
View file
Expand Up @@ -2441,6 +2441,10 @@ let CROSS_EMPTY = prove
(`(!s:A->bool. s CROSS {} = {}) /\ (!t:B->bool. {} CROSS t = {})`,
REWRITE_TAC[CROSS_EQ_EMPTY]);;

let CROSS_SING = prove
(`!x:A y:B. {x} CROSS {y} = {(x,y)}`,
REWRITE_TAC[EXTENSION; FORALL_PAIR_THM; IN_SING; IN_CROSS; PAIR_EQ]);;

let CROSS_UNIV = prove
(`(:A) CROSS (:B) = (:A#B)`,
REWRITE_TAC[CROSS; EXTENSION; IN_ELIM_PAIR_THM; FORALL_PAIR_THM; IN_UNIV]);;
Expand Down

0 comments on commit 2ef4029

Please sign in to comment.