---

Step * 1 of Lemma before-map


1. [T] : Type
2. [T'] : Type
3. f : T ⟶ T'
⊢ ∀x',y':T'.  (x' before y' ∈ [] ⇐⇒ ∃x,y:T. (x before y ∈ [] ∧ ((f x) = x' ∈ T') ∧ ((f y) = y' ∈ T')))
BY
{ (RWO "nil_before" 0 THEN Auto THEN ExRepD THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [T']  :  Type
3.  f  :  T  {}\mrightarrow{}  T'
\mvdash{}  \mforall{}x',y':T'.    (x'  before  y'  \mmember{}  []  \mLeftarrow{}{}\mRightarrow{}  \mexists{}x,y:T.  (x  before  y  \mmember{}  []  \mwedge{}  ((f  x)  =  x')  \mwedge{}  ((f  y)  =  y')))


By

---

Latex:
(RWO  "nil\_before"  0  THEN  Auto  THEN  ExRepD  THEN  Auto)

---

Home Index