---

Step * 1 1 of Lemma finite-quotient-bound


1. A : Type
2. R : A ⟶ A ⟶ ℙ
3. n : ℕ
4. A ~ ℕn
5. EquivRel(A;x,y.x R y)
6. ∀x,y:A.  Dec(x R y)
7. m : ℕ
8. x,y:A//(x R y) ~ ℕm
9. f : ℕn ⟶ A
10. Bij(ℕn;A;f)
11. Bij(x,y:ℕn//(x R_f y);x,y:A//(x R y);quo-lift(f))
12. EquivRel(ℕn;x,y.x R_f y)
13. x,y:ℕn//(x R_f y) ~ x,y:A//(x R y)
14. x,y:ℕn//(x R_f y) ~ ℕm
⊢ m ≤ n
BY
{ (Assert ⌜∀x,y:ℕn.  Dec(x R_f y)⌝⋅ THENA (RepUR ``preima_of_rel`` 0 THEN Auto)) }

1
1. A : Type
2. R : A ⟶ A ⟶ ℙ
3. n : ℕ
4. A ~ ℕn
5. EquivRel(A;x,y.x R y)
6. ∀x,y:A.  Dec(x R y)
7. m : ℕ
8. x,y:A//(x R y) ~ ℕm
9. f : ℕn ⟶ A
10. Bij(ℕn;A;f)
11. Bij(x,y:ℕn//(x R_f y);x,y:A//(x R y);quo-lift(f))
12. EquivRel(ℕn;x,y.x R_f y)
13. x,y:ℕn//(x R_f y) ~ x,y:A//(x R y)
14. x,y:ℕn//(x R_f y) ~ ℕm
15. ∀x,y:ℕn.  Dec(x R_f y)
⊢ m ≤ n

---

Latex:

---

Latex:

1.  A  :  Type
2.  R  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  n  :  \mBbbN{}
4.  A  \msim{}  \mBbbN{}n
5.  EquivRel(A;x,y.x  R  y)
6.  \mforall{}x,y:A.    Dec(x  R  y)
7.  m  :  \mBbbN{}
8.  x,y:A//(x  R  y)  \msim{}  \mBbbN{}m
9.  f  :  \mBbbN{}n  {}\mrightarrow{}  A
10.  Bij(\mBbbN{}n;A;f)
11.  Bij(x,y:\mBbbN{}n//(x  R\_f  y);x,y:A//(x  R  y);quo-lift(f))
12.  EquivRel(\mBbbN{}n;x,y.x  R\_f  y)
13.  x,y:\mBbbN{}n//(x  R\_f  y)  \msim{}  x,y:A//(x  R  y)
14.  x,y:\mBbbN{}n//(x  R\_f  y)  \msim{}  \mBbbN{}m
\mvdash{}  m  \mleq{}  n


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}x,y:\mBbbN{}n.    Dec(x  R\_f  y)\mkleeneclose{}\mcdot{}  THENA  (RepUR  ``preima\_of\_rel``  0  THEN  Auto))

---

Home Index