[ napply (. (ext_prop ā¦ Ha^-1)) | napply (. (ext_prop ā¦ Ha)) ] /2/.
nqed.
-unification hint 0 ā AA, x, S;
+unification hint 0 ā AA : setoid, S : š^AA, x : carr AA;
A ā carr AA,
SS ā (ext_carr ? S),
TT ā (mk_unary_morphism1 ??
- (Ī»x:setoid1_of_setoid ?.
+ (Ī»x:carr1 (setoid1_of_setoid ?).
mk_unary_morphism1 ??
- (Ī»S:ext_powerclass_setoid ?. x ā S)
- (prop11 ?? (mem_ext_powerclass_setoid_is_morph AA x)))
+ (Ī»S:carr1 (ext_powerclass_setoid ?). x ā (ext_carr ? S))
+ (prop11 ?? (fun11 ?? (mem_ext_powerclass_setoid_is_morph AA) x)))
(prop11 ?? (mem_ext_powerclass_setoid_is_morph AA))),
- XX ā (ext_powerclass_setoid AA)
- (*-------------------------------------*) ā¢
- fun11 (setoid1_of_setoid AA)
- (unary_morphism1_setoid1 XX CPROP) TT x S
- ā” mem A SS x.
+ T2 ā (ext_powerclass_setoid AA)
+(*---------------------------------------------------------------------------*) ā¢
+ fun11 T2 CPROP (fun11 (setoid1_of_setoid AA) (unary_morphism1_setoid1 T2 CPROP) TT x) S ā” mem A SS x.
nlemma set_ext : āS.āA,B:Ī©^S.A =_1 B ā āx:S.(x ā A) =_1 (x ā B).
#S A B; *; #H1 H2 x; @; ##[ napply H1 | napply H2] nqed.
nqed.
alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ā
- A : setoid, B,C : ext_powerclass A;
- R ā (mk_ext_powerclass ? (B ā© C) (ext_prop ? (intersect_is_ext ? B C)))
+unification hint 0 ā A : setoid, B,C : š^A;
+ AA ā carr A,
+ BB ā ext_carr ? B,
+ CC ā ext_carr ? C,
+ R ā (mk_ext_powerclass ?
+ (ext_carr ? B ā© ext_carr ? C)
+ (ext_prop ? (intersect_is_ext ? B C)))
(* ------------------------------------------*) ā¢
- ext_carr A R ā” intersect ? (ext_carr ? B) (ext_carr ? C).
+ ext_carr A R ā” intersect AA BB CC.
nlemma intersect_is_morph: āA. Ī©^A ā_1 Ī©^A ā_1 Ī©^A.
#A; napply (mk_binary_morphism1 ā¦ (Ī»S,S'. S ā© S'));
unification hint 0 ā A : Type[0], B,C : Ī©^A;
T ā powerclass_setoid A,
R ā mk_unary_morphism1 ??
- (Ī»S. mk_unary_morphism1 ?? (Ī»S'.S ā© S') (prop11 ?? (intersect_is_morph A S)))
+ (Ī»X. mk_unary_morphism1 ??
+ (Ī»Y.X ā© Y) (prop11 ?? (fun11 ?? (intersect_is_morph A) X)))
(prop11 ?? (intersect_is_morph A))
(*------------------------------------------------------------------------*) ā¢
fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C ā” intersect A B C.
AA : setoid, B,C : š^AA;
A ā carr AA,
T ā ext_powerclass_setoid AA,
- R ā (mk_unary_morphism1 ??
- (Ī»S:š^AA.
- mk_unary_morphism1 ??
- (Ī»S':š^AA.
- mk_ext_powerclass AA (Sā©S') (ext_prop AA (intersect_is_ext ? S S')))
- (prop11 ?? (intersect_is_ext_morph AA S)))
+ R ā (mk_unary_morphism1 ?? (Ī»X:š^AA.
+ mk_unary_morphism1 ?? (Ī»Y:š^AA.
+ mk_ext_powerclass AA
+ (ext_carr ? X ā© ext_carr ? Y)
+ (ext_prop AA (intersect_is_ext ? X Y)))
+ (prop11 ?? (fun11 ?? (intersect_is_ext_morph AA) X)))
(prop11 ?? (intersect_is_ext_morph AA))) ,
BB ā (ext_carr ? B),
CC ā (ext_carr ? C)
nqed.
alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ā
- A : setoid, B,C : š^A;
- R ā (mk_ext_powerclass ? (B āŖ C) (ext_prop ? (union_is_ext ? B C)))
+unification hint 0 ā A : setoid, B,C : š^A;
+ AA ā carr A,
+ BB ā ext_carr ? B,
+ CC ā ext_carr ? C,
+ R ā mk_ext_powerclass ?
+ (ext_carr ? B āŖ ext_carr ? C) (ext_prop ? (union_is_ext ? B C))
(*-------------------------------------------------------------------------*) ā¢
- ext_carr A R ā” union ? (ext_carr ? B) (ext_carr ? C).
+ ext_carr A R ā” union AA BB CC.
unification hint 0 ā S:Type[0], A,B:Ī©^S;
T ā powerclass_setoid S,
MM ā mk_unary_morphism1 ??
- (Ī»A.mk_unary_morphism1 ?? (Ī»B.A āŖ B) (prop11 ?? (union_is_morph S A)))
+ (Ī»A.mk_unary_morphism1 ??
+ (Ī»B.A āŖ B) (prop11 ?? (fun11 ?? (union_is_morph S) A)))
(prop11 ?? (union_is_morph S))
(*--------------------------------------------------------------------------*) ā¢
fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ā” A āŖ B.
AA : setoid, B,C : š^AA;
A ā carr AA,
T ā ext_powerclass_setoid AA,
- R ā (mk_unary_morphism1 ??
- (Ī»S:š^AA.
- mk_unary_morphism1 ??
- (Ī»S':š^AA.
- mk_ext_powerclass AA (S āŖ S') (ext_prop AA (union_is_ext ? S S')))
- (prop11 ?? (union_is_ext_morph AA S)))
- (prop11 ?? (union_is_ext_morph AA))) ,
+ R ā mk_unary_morphism1 ?? (Ī»X:š^AA.
+ mk_unary_morphism1 ?? (Ī»Y:š^AA.
+ mk_ext_powerclass AA
+ (ext_carr ? X āŖ ext_carr ? Y) (ext_prop AA (union_is_ext ? X Y)))
+ (prop11 ?? (fun11 ?? (union_is_ext_morph AA) X)))
+ (prop11 ?? (union_is_ext_morph AA)),
BB ā (ext_carr ? B),
CC ā (ext_carr ? C)
(*------------------------------------------------------*) ā¢
nqed.
alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ā
- A : setoid, B,C : š^A;
- R ā (mk_ext_powerclass ? (B - C) (ext_prop ? (substract_is_ext ? B C)))
-(*-------------------------------------------------------------------------*) ā¢
- ext_carr A R ā” substract ? (ext_carr ? B) (ext_carr ? C).
+unification hint 0 ā A : setoid, B,C : š^A;
+ AA ā carr A,
+ BB ā ext_carr ? B,
+ CC ā ext_carr ? C,
+ R ā mk_ext_powerclass ?
+ (ext_carr ? B - ext_carr ? C)
+ (ext_prop ? (substract_is_ext ? B C))
+(*---------------------------------------------------*) ā¢
+ ext_carr A R ā” substract AA BB CC.
unification hint 0 ā S:Type[0], A,B:Ī©^S;
T ā powerclass_setoid S,
MM ā mk_unary_morphism1 ??
- (Ī»A.mk_unary_morphism1 ?? (Ī»B.A - B) (prop11 ?? (substract_is_morph S A)))
+ (Ī»A.mk_unary_morphism1 ??
+ (Ī»B.A - B) (prop11 ?? (fun11 ?? (substract_is_morph S) A)))
(prop11 ?? (substract_is_morph S))
(*--------------------------------------------------------------------------*) ā¢
fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ā” A - B.
AA : setoid, B,C : š^AA;
A ā carr AA,
T ā ext_powerclass_setoid AA,
- R ā (mk_unary_morphism1 ??
- (Ī»S:š^AA.
- mk_unary_morphism1 ??
- (Ī»S':š^AA.
- mk_ext_powerclass AA (S - S') (ext_prop AA (substract_is_ext ? S S')))
- (prop11 ?? (substract_is_ext_morph AA S)))
- (prop11 ?? (substract_is_ext_morph AA))) ,
+ R ā mk_unary_morphism1 ?? (Ī»X:š^AA.
+ mk_unary_morphism1 ?? (Ī»Y:š^AA.
+ mk_ext_powerclass AA
+ (ext_carr ? X - ext_carr ? Y)
+ (ext_prop AA (substract_is_ext ? X Y)))
+ (prop11 ?? (fun11 ?? (substract_is_ext_morph AA) X)))
+ (prop11 ?? (substract_is_ext_morph AA)),
BB ā (ext_carr ? B),
CC ā (ext_carr ? C)
(*------------------------------------------------------*) ā¢
#X a; @; ##[ napply ({(a)}); ##] #x y E; @; #H; /3/; nqed.
alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ā A : setoid, a:A;
+unification hint 0 ā A : setoid, a : carr A;
R ā (mk_ext_powerclass ? {(a)} (ext_prop ? (single_is_ext ? a)))
(*-------------------------------------------------------------------------*) ā¢
ext_carr A R ā” singleton A a.
-unification hint 0 ā A:setoid, a:A;
+unification hint 0 ā A:setoid, a : carr A;
T ā setoid1_of_setoid A,
AA ā carr A,
MM ā mk_unary_morphism1 ??
- (Ī»a:setoid1_of_setoid A.{(a)}) (prop11 ?? (single_is_morph A))
+ (Ī»a:carr1 (setoid1_of_setoid A).{(a)}) (prop11 ?? (single_is_morph A))
(*--------------------------------------------------------------------------*) ā¢
fun11 T (powerclass_setoid AA) MM a ā” {(a)}.
nlemma single_is_ext_morph:āA:setoid.(setoid1_of_setoid A) ā_1 š^A.
#A; @; ##[ #a; napply (single_is_ext ? a); ##] #a b E; @; #x; /3/; nqed.
-unification hint 1 ā
- AA : setoid, a: AA;
+unification hint 1 ā AA : setoid, a: carr AA;
T ā ext_powerclass_setoid AA,
R ā mk_unary_morphism1 ??
- (Ī»a:setoid1_of_setoid AA.
+ (Ī»a:carr1 (setoid1_of_setoid AA).
mk_ext_powerclass AA {(a)} (ext_prop ? (single_is_ext AA a)))
(prop11 ?? (single_is_ext_morph AA))
(*------------------------------------------------------*) ā¢
ext_carr AA (fun11 (setoid1_of_setoid AA) T R a) ā” singleton AA a.
-
-
-
-
(*
alias symbol "hint_decl" = "hint_decl_Type2".
unification hint 0 ā