---

Step * 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
⊢ m ≤ n
BY
{ ((Assert ℕn ~ A BY
          (RelRST THEN Auto))
   THEN D -1
   THEN (InstLemma `biject-quotient` [⌜ℕn⌝;⌜A⌝;⌜f⌝;⌜R⌝]⋅ THENA Auto)
   THEN (Assert EquivRel(ℕn;x,y.x R_f y) BY
               (BLemma `preima_of_equiv_rel` THEN Auto))
   THEN (Assert x,y:ℕn//(x R_f y) ~ x,y:A//(x R y) BY
               (D 0 With ⌜quo-lift(f)⌝  THEN Auto))
   THEN (Assert x,y:ℕn//(x R_f y) ~ ℕm BY
               (RelRST 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
⊢ 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
\mvdash{}  m  \mleq{}  n


By

---

Latex:
((Assert  \mBbbN{}n  \msim{}  A  BY
                (RelRST  THEN  Auto))
  THEN  D  -1
  THEN  (InstLemma  `biject-quotient`  [\mkleeneopen{}\mBbbN{}n\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  EquivRel(\mBbbN{}n;x,y.x  R\_f  y)  BY
                          (BLemma  `preima\_of\_equiv\_rel`  THEN  Auto))
  THEN  (Assert  x,y:\mBbbN{}n//(x  R\_f  y)  \msim{}  x,y:A//(x  R  y)  BY
                          (D  0  With  \mkleeneopen{}quo-lift(f)\mkleeneclose{}    THEN  Auto))
  THEN  (Assert  x,y:\mBbbN{}n//(x  R\_f  y)  \msim{}  \mBbbN{}m  BY
                          (RelRST  THEN  Auto)))

---

Home Index