Step
*
of Lemma
cond_rel_star_equiv
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R1,E:T ⟶ T ⟶ ℙ].
(EquivRel(T)(_1 E _2)
⇒ when P, R1 => E
⇒ R1 preserves P
⇒ when P, R1^* => E)
BY
{ Auto }
1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. [R1] : T ⟶ T ⟶ ℙ
4. [E] : T ⟶ T ⟶ ℙ
5. EquivRel(T)(_1 E _2)
6. when P, R1 => E
7. R1 preserves P
⊢ when P, R1^* => E
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[P:T {}\mrightarrow{} \mBbbP{}]. \mforall{}[R1,E:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}].
(EquivRel(T)($_{1}$ E $_{2}$) {}\mRightarrow{} when P, R1 => E {}\mRightarrow{} R1 pre\000Cserves P {}\mRightarrow{} when P, rel\_star(T; R1) => E)
By
Latex:
Auto
Home
Index