---

Step * of Lemma locl-pre-preserving-1-1

∀[es:EO]. ∀[P:E ─→ ℙ]. ∀[f:{e:E| P e}  ─→ E].  Inj({e:E| P e} ;E;f) supposing f is locl-pre-preserving on P
BY
{ (RepUR ``locl-pre-preserving rel-pre-preserving`` 0 THEN Auto) }

1
1. es : EO
2. P : E ─→ ℙ
3. f : {e:E| P e}  ─→ E
4. f is λe,e'. e ≤loc e' -λe,e'. e ≤loc e' -pre-preserving on P
⊢ Inj({e:E| P e} ;E;f)

---

Latex:


\mforall{}[es:EO].  \mforall{}[P:E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[f:\{e:E|  P  e\}    {}\mrightarrow{}  E].
    Inj(\{e:E|  P  e\}  ;E;f)  supposing  f  is  locl-pre-preserving  on  P


By

(RepUR  ``locl-pre-preserving  rel-pre-preserving``  0  THEN  Auto)

---

Home Index