---

Step * 3 of Lemma pairs-fpf_property


1. [A] : Type
2. [B] : Type
3. eq1 : EqDecider(A)@i
4. eq2 : EqDecider(B)@i
5. L : (A × B) List@i
6. no_repeats(A;fpf-domain(fpf(L)))
7. ∀a:A. ((a ∈ fpf-domain(fpf(L))) ⇐⇒ ∃b:B. (<a, b> ∈ L))
⊢ ∀a∈dom(fpf(L)). l=fpf(L)(a) ⇒  no_repeats(B;l) ∧ (∀b:B. ((b ∈ l) ⇐⇒ (<a, b> ∈ L)))
BY
{ (RepeatFor 3 ((D 0 THENA Auto)))⋅ }

1
1. [A] : Type
2. [B] : Type
3. eq1 : EqDecider(A)@i
4. eq2 : EqDecider(B)@i
5. L : (A × B) List@i
6. no_repeats(A;fpf-domain(fpf(L)))
7. ∀a:A. ((a ∈ fpf-domain(fpf(L))) ⇐⇒ ∃b:B. (<a, b> ∈ L))
8. a : A@i
9. ↑a ∈ dom(fpf(L))@i
⊢ no_repeats(B;fpf(L)(a))

2
1. [A] : Type
2. [B] : Type
3. eq1 : EqDecider(A)@i
4. eq2 : EqDecider(B)@i
5. L : (A × B) List@i
6. no_repeats(A;fpf-domain(fpf(L)))
7. ∀a:A. ((a ∈ fpf-domain(fpf(L))) ⇐⇒ ∃b:B. (<a, b> ∈ L))
8. a : A@i
9. ↑a ∈ dom(fpf(L))@i
⊢ ∀b:B. ((b ∈ fpf(L)(a)) ⇐⇒ (<a, b> ∈ L))

---

Latex:



1.  [A]  :  Type
2.  [B]  :  Type
3.  eq1  :  EqDecider(A)@i
4.  eq2  :  EqDecider(B)@i
5.  L  :  (A  \mtimes{}  B)  List@i
6.  no\_repeats(A;fpf-domain(fpf(L)))
7.  \mforall{}a:A.  ((a  \mmember{}  fpf-domain(fpf(L)))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}b:B.  (<a,  b>  \mmember{}  L))
\mvdash{}  \mforall{}a\mmember{}dom(fpf(L)).  l=fpf(L)(a)  {}\mRightarrow{}    no\_repeats(B;l)  \mwedge{}  (\mforall{}b:B.  ((b  \mmember{}  l)  \mLeftarrow{}{}\mRightarrow{}  (<a,  b>  \mmember{}  L)))


By

(RepeatFor  3  ((D  0  THENA  Auto)))\mcdot{}

---

Home Index