---

Step * 1 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. f : a:A ⟶ B[a]
7. g : Base
8. h : Base
9. h = f ∈ (a:A ⟶ B[a])
10. h ≤ g
11. a : A
12. mono(B[a])
⊢ (f a) = (g a) ∈ B[a]
BY
{ (With ⌜f a⌝ (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. f : a:A ⟶ B[a]
7. g : Base
8. h : Base
9. h = f ∈ (a:A ⟶ B[a])
10. h ≤ g
11. a : A
12. ∀b:Base. (is-above(B[a];f a;b) ⇒ ((f a) = b ∈ B[a]))
⊢ (f a) = (g a) ∈ 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.  f  :  a:A  {}\mrightarrow{}  B[a]
7.  g  :  Base
8.  h  :  Base
9.  h  =  f
10.  h  \mleq{}  g
11.  a  :  A
12.  mono(B[a])
\mvdash{}  (f  a)  =  (g  a)


By

---

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

---

Home Index