---

Step * 1 of Lemma surject-inverse


1. [A] : Type
2. [B] : Type
3. f : A ⟶ B
4. Surj(A;B;f)
⊢ ∃g:B ⟶ A. ∀x:B. ((f (g x)) = x ∈ B)
BY
{ (Unfold `surject` -1 THEN RenameVar `g' (-1) THEN (InstConcl [⌜λb.(fst((g b)))⌝]⋅ THEN Auto) THEN Reduce 0) }

1
1. A : Type
2. B : Type
3. f : A ⟶ B
4. g : ∀b:B. ∃a:A. ((f a) = b ∈ B)
5. x : B
⊢ (f (fst((g x)))) = x ∈ B

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  Surj(A;B;f)
\mvdash{}  \mexists{}g:B  {}\mrightarrow{}  A.  \mforall{}x:B.  ((f  (g  x))  =  x)


By

---

Latex:
(Unfold  `surject`  -1
  THEN  RenameVar  `g'  (-1)
  THEN  (InstConcl  [\mkleeneopen{}\mlambda{}b.(fst((g  b)))\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  Reduce  0)

---

Home Index