Step
*
of Lemma
preserved_by_or
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  (R1 preserves P 
⇒ R2 preserves P 
⇒ R1 ∨ R2 preserves P)
BY
{ (Unfolds ``rel_or preserved_by`` 0 THEN Reduce 0 THEN Auto THEN (D (-1))) }
1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. [R1] : T ⟶ T ⟶ ℙ
4. [R2] : T ⟶ T ⟶ ℙ
5. ∀x,y:T.  ((P x) 
⇒ (x R1 y) 
⇒ (P y))
6. ∀x,y:T.  ((P x) 
⇒ (x R2 y) 
⇒ (P y))
7. x : T
8. y : T
9. P x
10. x R1 y
⊢ P y
2
1. [T] : Type
2. [P] : T ⟶ ℙ
3. [R1] : T ⟶ T ⟶ ℙ
4. [R2] : T ⟶ T ⟶ ℙ
5. ∀x,y:T.  ((P x) 
⇒ (x R1 y) 
⇒ (P y))
6. ∀x,y:T.  ((P x) 
⇒ (x R2 y) 
⇒ (P y))
7. x : T
8. y : T
9. P x
10. x R2 y
⊢ P y
Latex:
Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (R1  preserves  P  {}\mRightarrow{}  R2  preserves  P  {}\mRightarrow{}  R1  \mvee{}  R2  preserves  P)
By
Latex:
(Unfolds  ``rel\_or  preserved\_by``  0  THEN  Reduce  0  THEN  Auto  THEN  (D  (-1)))
Home
Index