---

Step * 1 1 1 2 1 1 1 1 2 1 of Lemma function-mono


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. g : Base
7. h : Base
8. h ≤ g
9. a : Base
10. b : Base
11. c : a = b ∈ A
12. h ∈ a:A ⟶ B[a]
13. mono(B[b])
⊢ (h b) = (g b) ∈ B[a]
BY
{ (With ⌜h b⌝ (D (-1))⋅ THENA Auto) }

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. g : Base
7. h : Base
8. h ≤ g
9. a : Base
10. b : Base
11. c : a = b ∈ A
12. h ∈ a:A ⟶ B[a]
13. ∀b@0:Base. (is-above(B[b];h b;b@0) ⇒ ((h b) = b@0 ∈ B[b]))
⊢ (h b) = (g b) ∈ B[a]

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  A  \msubseteq{}r  Base
4.  \mforall{}a:A.  mono(B[a])
5.  \mexists{}a:A.  value-type(B[a])
6.  g  :  Base
7.  h  :  Base
8.  h  \mleq{}  g
9.  a  :  Base
10.  b  :  Base
11.  c  :  a  =  b
12.  h  \mmember{}  a:A  {}\mrightarrow{}  B[a]
13.  mono(B[b])
\mvdash{}  (h  b)  =  (g  b)


By

---

Latex:
(With  \mkleeneopen{}h  b\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)

---

Home Index