---

Step * of Lemma function-mono

∀A:Type. ∀B:A ⟶ Type.  (((A ⊆r Base) ∧ (∀a:A. mono(B[a])) ∧ (↓∃a:A. value-type(B[a]))) ⇒ mono(a:A ⟶ B[a]))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN RenameVar `f' (-1)
   THEN Auto
   THEN RenameVar `g' (-2)
   THEN RepeatFor 2 (D -1)
   THEN RenameVar `h' (-3)) }

1
1. A : Type
2. B : A ⟶ Type
3. A ⊆r Base
4. ∀a:A. mono(B[a])
5. ∃a:A. value-type(B[a])
6. f : a:A ⟶ B[a]
7. g : Base
8. h : Base
9. h = f ∈ (a:A ⟶ B[a])
10. h ≤ g
⊢ f = g ∈ (a:A ⟶ B[a])

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}B:A  {}\mrightarrow{}  Type.
    (((A  \msubseteq{}r  Base)  \mwedge{}  (\mforall{}a:A.  mono(B[a]))  \mwedge{}  (\mdownarrow{}\mexists{}a:A.  value-type(B[a])))  {}\mRightarrow{}  mono(a:A  {}\mrightarrow{}  B[a]))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  RenameVar  `f'  (-1)
  THEN  Auto
  THEN  RenameVar  `g'  (-2)
  THEN  RepeatFor  2  (D  -1)
  THEN  RenameVar  `h'  (-3))

---

Home Index