---

Step * of Lemma bigrel-iff

∀[T:Type]
  ∀F:(T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ
    (rel-monotone{i:l}(T;R.F[R]) ⇒ rel-continuous{i:l}(T;R.F[R]) ⇒ (∨R.F[R] => F[∨R.F[R]] ∧ F[∨R.F[R]] => ∨R.F[R]))
BY
{ Auto }

1
1. [T] : Type
2. F : (T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ
3. rel-monotone{i:l}(T;R.F[R])
4. rel-continuous{i:l}(T;R.F[R])
⊢ ∨R.F[R] => F[∨R.F[R]]

2
1. [T] : Type
2. F : (T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ
3. rel-monotone{i:l}(T;R.F[R])
4. rel-continuous{i:l}(T;R.F[R])
5. ∨R.F[R] => F[∨R.F[R]]
⊢ F[∨R.F[R]] => ∨R.F[R]

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}F:(T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
        (rel-monotone\{i:l\}(T;R.F[R])
        {}\mRightarrow{}  rel-continuous\{i:l\}(T;R.F[R])
        {}\mRightarrow{}  (\mvee{}R.F[R]  =>  F[\mvee{}R.F[R]]  \mwedge{}  F[\mvee{}R.F[R]]  =>  \mvee{}R.F[R]))


By

---

Latex:
Auto

---

Home Index