---

Step * 1 of Lemma sq_stable__sorted-by


1. [T] : Type
2. L : T List
3. [R] : {x:T| (x ∈ L)}  ⟶ {x:T| (x ∈ L)}  ⟶ ℙ
4. ∀x,y:{x:T| (x ∈ L)} .  SqStable(R x y)
5. Z : {x:T| (x ∈ L)}  List
6. L = Z ∈ ({x:T| (x ∈ L)}  List)
⊢ SqStable(sorted-by(R;Z))
BY
{ (RepUR ``sorted-by`` 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  [R]  :  \{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x,y:\{x:T|  (x  \mmember{}  L)\}  .    SqStable(R  x  y)
5.  Z  :  \{x:T|  (x  \mmember{}  L)\}    List
6.  L  =  Z
\mvdash{}  SqStable(sorted-by(R;Z))


By

---

Latex:
(RepUR  ``sorted-by``  0  THEN  Auto)\mcdot{}

---

Home Index