(* ----------------------------------------------------- *) ⊢
carr1 R ≡ ext_powerclass A.
-
+interpretation "prop21 mem" 'prop2 l r = (prop21 (setoid1_of_setoid ?) (ext_powerclass_setoid ?) ? ? ???? l r).
+
(*
ncoercion ext_carr' : ∀A.∀x:ext_powerclass_setoid A. Ω^A ≝ ext_carr
on _x : (carr1 (ext_powerclass_setoid ?)) to (Ω^?).
nlemma intersect_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A.
#A; #S; #S'; @ (S ∩ S');
- #a; #a'; #Ha; @; *; #H1; #H2; @
+ #a; #a'; #Ha; @; *; #H1; #H2; @
[##1,2: napply (. Ha^-1‡#); nassumption;
##|##3,4: napply (. Ha‡#); nassumption]
nqed.
fun21 (powerclass_setoid A) (powerclass_setoid A) (powerclass_setoid A) R B C
≡ intersect ? B C.
-interpretation "prop21 mem" 'prop2 l r = (prop21 (setoid1_of_setoid ?) (ext_powerclass_setoid ?) ? ???? l r).
-interpretation "prop21 ext" 'prop2 l r = (prop21 (ext_powerclass_setoid ?) (ext_powerclass_setoid ?) ? ???? l r).
+interpretation "prop21 ext" 'prop2 l r = (prop21 (ext_powerclass_setoid ?) (ext_powerclass_setoid ?) ? ? ???? l r).
nlemma intersect_is_ext_morph:
∀A. binary_morphism1 (ext_powerclass_setoid A) (ext_powerclass_setoid A) (ext_powerclass_setoid A).
unification hint 0 ≔
A, B : CPROP ⊢ iff A B ≡ eq_rel1 ? (eq1 CPROP) A B.
-*)
nlemma test: ∀U.∀A,B:𝛀^U. A ∩ B = A →
∀x,y. x=y → x ∈ A → y ∈ A ∩ B.
#U; #A; #B; #H; #x; #y; #K; #K2;
-napply (. (prop21 ??? ? ???? K^-1 (H^-1‡#)));
+ alias symbol "prop2" = "prop21 mem".
+ alias symbol "invert" = "setoid1 symmetry".
+ napply (. K^-1‡H);
nassumption;
nqed.
##|##3,4: napply (. Ha‡#); nassumption]##]
##| #a; #a'; #b; #b'; #Ha; #Hb; nwhd; @; #x; nwhd in ⊢ (% → %); #H
[ alias symbol "invert" = "setoid1 symmetry".
- napply (. ((#‡Ha^-1)‡(#‡Hb^-1))); nassumption
+ alias symbol "refl" = "refl".
+alias symbol "prop2" = "prop21".
+napply (. ((#‡Ha^-1)‡(#‡Hb^-1))); nassumption
| napply (. ((#‡Ha)‡(#‡Hb))); nassumption ]##]
nqed.
(* unfold if intersect, exposing fun21 *)
alias symbol "hint_decl" = "hint_decl_Type1".
unification hint 0 ≔
- A : setoid, B,C : qpowerclass A ⊢
+ A : setoid, B,C : ext_powerclass A ⊢
pc A (fun21 …
(mk_binary_morphism1 …
(λS,S':qpowerclass_setoid A.mk_qpowerclass ? (S ∩ S') (mem_ok' ? (intersect_ok ? S S')))
#A; #U; #V; #x; #x'; #H; #p; napply (. (H^-1‡#)); nassumption.
nqed.
*)
-*)
ndefinition image: ∀A,B. (carr A → carr B) → Ω^A → Ω^B ≝
λA,B:setoid.λf:carr A → carr B.λSa:Ω^A.
#A; #B; #f; #x; napply refl;
nqed.
+alias symbol "eq" = "setoid eq".
ndefinition surjective ≝
λA,B.λS: ext_powerclass A.λT: ext_powerclass B.λf:unary_morphism A B.
∀y. y ∈ T → ∃x. x ∈ S ∧ f x = y.
f_inj: injective … S iso_f
}.
+nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W.
+#A; #U; #V; #W; *; #H; #x; *; #xU; #xV; napply H; nassumption;
+nqed.
+
+nlemma subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W.
+#A; #U; #V; #W; #H; #H1; #x; *; #Hx; ##[ napply H; ##| napply H1; ##] nassumption;
+nqed.
+
+nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V.
+#A; #U; #V; #W; #H1; #H2; #x; #Hx; @; ##[ napply H1; ##| napply H2; ##] nassumption;
+nqed.
+
(*
nrecord isomorphism (A, B : setoid) (S: qpowerclass A) (T: qpowerclass B) : CProp[0] ≝
{ iso_f:> unary_morphism A B;