---

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