---

Step * of Lemma monot_shift

∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ].
  ∀opa:A ⟶ A. ∀opb:B ⟶ B. ∀f:A ⟶ B.
    RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f) ⇒ monot(B;x,y.S[x;y];opb) ⇒ monot(A;x,y.R[x;y];opa) 
    supposing fun_thru_1op(A;B;opa;opb;f)
BY
{ ((Unfold `so_apply` 0 
THEN ARepD ["basic"]) THENA Auto) }

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

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[S:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}opa:A  {}\mrightarrow{}  A.  \mforall{}opb:B  {}\mrightarrow{}  B.  \mforall{}f:A  {}\mrightarrow{}  B.
        RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f)  {}\mRightarrow{}  monot(B;x,y.S[x;y];opb)  {}\mRightarrow{}  monot(A;x,y.R[x;y];opa) 
        supposing  fun\_thru\_1op(A;B;opa;opb;f)


By

---

Latex:
((Unfold  `so\_apply`  0 
THEN  ARepD  ["basic"])  THENA  Auto)

---

Home Index