---

Step * of Lemma rel-pre-preserving-compose

∀es:EO
  ∀[P,Q:E ⟶ ℙ]. ∀[R:E ⟶ E ⟶ ℙ].
    ∀f1:{e:E| P e}  ⟶ {e:E| Q e} . ∀f2:{e:E| Q e}  ⟶ E.
      ((f1 is R-pre-preserving on P ∧ f2 is R-pre-preserving on Q) ⇒ f2 o f1 is R-pre-preserving on P)
BY
{ Unfold `rel-pre-preserving` 0 }

1
∀es:EO
  ∀[P,Q:E ⟶ ℙ]. ∀[R:E ⟶ E ⟶ ℙ].
    ∀f1:{e:E| P e}  ⟶ {e:E| Q e} . ∀f2:{e:E| Q e}  ⟶ E.
      ((f1 is R-R-pre-preserving on P ∧ f2 is R-R-pre-preserving on Q) ⇒ f2 o f1 is R-R-pre-preserving on P)

---

Latex:

---

Latex:
\mforall{}es:EO
    \mforall{}[P,Q:E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].
        \mforall{}f1:\{e:E|  P  e\}    {}\mrightarrow{}  \{e:E|  Q  e\}  .  \mforall{}f2:\{e:E|  Q  e\}    {}\mrightarrow{}  E.
            ((f1  is  R-pre-preserving  on  P  \mwedge{}  f2  is  R-pre-preserving  on  Q)
            {}\mRightarrow{}  f2  o  f1  is  R-pre-preserving  on  P)


By

---

Latex:
Unfold  `rel-pre-preserving`  0

---

Home Index