---

Step * 1 1 of Lemma union_functionality_wrt_equipollent


1. [A] : Type
2. [B] : Type
3. [C] : Type
4. [D] : Type
5. f : A ⟶ B@i
6. Bij(A;B;f)
7. g : C ⟶ D@i
8. Bij(C;D;g)
⊢ Bij(A + C;B + D;λx.case x of inl(a) => inl (f a) | inr(c) => inr (g c) )
BY
{ TACTIC:(RepeatFor 2 (D 0) THEN (Reduce 0 THENA Auto) THEN D -1 THEN Reduce 0 THEN Auto) }

1
1. A : Type
2. B : Type
3. C : Type
4. D : Type
5. f : A ⟶ B@i
6. Bij(A;B;f)
7. g : C ⟶ D@i
8. Bij(C;D;g)
9. x : A@i
10. a2 : A + C@i
11. (inl (f x)) = case a2 of inl(a) => inl (f a) | inr(c) => inr (g c)  ∈ (B + D)
⊢ (inl x) = a2 ∈ (A + C)

2
1. A : Type
2. B : Type
3. C : Type
4. D : Type
5. f : A ⟶ B@i
6. Bij(A;B;f)
7. g : C ⟶ D@i
8. Bij(C;D;g)
9. y : C@i
10. a2 : A + C@i
11. (inr (g y) ) = case a2 of inl(a) => inl (f a) | inr(c) => inr (g c)  ∈ (B + D)
⊢ (inr y ) = a2 ∈ (A + C)

3
1. [A] : Type
2. [B] : Type
3. [C] : Type
4. [D] : Type
5. f : A ⟶ B@i
6. Bij(A;B;f)
7. g : C ⟶ D@i
8. Bij(C;D;g)
9. x : B@i
⊢ ∃a:A + C. (case a of inl(a) => inl (f a) | inr(c) => inr (g c)  = (inl x) ∈ (B + D))

4
1. [A] : Type
2. [B] : Type
3. [C] : Type
4. [D] : Type
5. f : A ⟶ B@i
6. Bij(A;B;f)
7. g : C ⟶ D@i
8. Bij(C;D;g)
9. y : D@i
⊢ ∃a:A + C. (case a of inl(a) => inl (f a) | inr(c) => inr (g c)  = (inr y ) ∈ (B + D))

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  [C]  :  Type
4.  [D]  :  Type
5.  f  :  A  {}\mrightarrow{}  B@i
6.  Bij(A;B;f)
7.  g  :  C  {}\mrightarrow{}  D@i
8.  Bij(C;D;g)
\mvdash{}  Bij(A  +  C;B  +  D;\mlambda{}x.case  x  of  inl(a)  =>  inl  (f  a)  |  inr(c)  =>  inr  (g  c)  )


By

---

Latex:
TACTIC:(RepeatFor  2  (D  0)  THEN  (Reduce  0  THENA  Auto)  THEN  D  -1  THEN  Reduce  0  THEN  Auto)

---

Home Index