---

Step * of Lemma utrans_shift

∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ].
  ∀f:A ⟶ B
    ((∀[x,y:A].  R[x;y] supposing R[x;y])
    ⇒ RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f)
    ⇒ UniformlyTrans(B;x,y.S[x;y])
    ⇒ UniformlyTrans(A;x,y.R[x;y]))
BY
{ ((ARepD ["basic"]) THENA Auto) }

1
1. [A] : Type
2. [B] : Type
3. [R] : A ⟶ A ⟶ ℙ
4. [S] : B ⟶ B ⟶ ℙ
5. f : A ⟶ B@i
6. ∀[x,y:A].  R[x;y] supposing R[x;y]@i
7. ∀x,y:A.  (R[x;y] ⇐⇒ S[f x;f y])@i
8. ∀[a,b,c:B].  (S[a;b] ⇒ S[b;c] ⇒ S[a;c])@i
9. [a] : A
10. [b] : A
11. [c] : A
12. R[a;b]@i
13. R[b;c]@i
⊢ R[a;c]

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[S:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}f:A  {}\mrightarrow{}  B
        ((\mforall{}[x,y:A].    R[x;y]  supposing  R[x;y])
        {}\mRightarrow{}  RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f)
        {}\mRightarrow{}  UniformlyTrans(B;x,y.S[x;y])
        {}\mRightarrow{}  UniformlyTrans(A;x,y.R[x;y]))


By

---

Latex:
((ARepD  ["basic"])  THENA  Auto)

---

Home Index