---

Step * of Lemma symmetrized_preorder

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (Preorder(T;x,y.R[x;y]) ⇒ EquivRel(T;a,b.Symmetrize(x,y.R[x;y];a;b)))
BY
{ (Unfolds ``preorder equiv_rel symmetrize`` 0 THEN Auto) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. Refl(T;x,y.R[x;y])
4. Trans(T;x,y.R[x;y])
⊢ Refl(T;a,b.R[a;b] ∧ R[b;a])

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. Refl(T;x,y.R[x;y])
4. Trans(T;x,y.R[x;y])
5. Refl(T;a,b.R[a;b] ∧ R[b;a])
⊢ Sym(T;a,b.R[a;b] ∧ R[b;a])

3
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. Refl(T;x,y.R[x;y])
4. Trans(T;x,y.R[x;y])
5. Refl(T;a,b.R[a;b] ∧ R[b;a])
6. Sym(T;a,b.R[a;b] ∧ R[b;a])
⊢ Trans(T;a,b.R[a;b] ∧ R[b;a])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (Preorder(T;x,y.R[x;y])  {}\mRightarrow{}  EquivRel(T;a,b.Symmetrize(x,y.R[x;y];a;b)))


By

---

Latex:
(Unfolds  ``preorder  equiv\_rel  symmetrize``  0  THEN  Auto)

---

Home Index