---

Step * of Lemma funinv_wf

∀[n,m:ℕ]. ∀[f:{f:ℕn ⟶ ℕm| Surj(ℕn;ℕm;f)} ].  (inv(f) ∈ {g:ℕm ⟶ ℕn| Inj(ℕm;ℕn;g) ∧ (∀x:ℕm. ((f (g x)) = x ∈ ℤ))} )
BY
{ (Auto
   THEN D -1
   THEN Unfold `surject` -1
   THEN (Assert ∀x:ℕm. ((inv(f) x ∈ ℕn) ∧ (↑(f (inv(f) x) =z x)) ∧ (∀[i:ℕn]. ¬↑(f i =z x) supposing i < inv(f) x)) BY
               (ParallelLast
                THEN ((InstLemma `mu-bound-property+` [⌜n⌝;⌜λn.(f n =z x)⌝]⋅ THENA Auto)
                THENM (RepUR ``funinv`` 0 THEN Reduce (-1) THEN Trivial)
                )
                THEN Reduce 0
                THEN RW assert_pushdownC 0
                THEN Auto
                THEN ParallelLast
                THEN Auto))) }

1
1. n : ℕ
2. m : ℕ
3. f : ℕn ⟶ ℕm
4. ∀b:ℕm. ∃a:ℕn. ((f a) = b ∈ ℕm)
5. ∀x:ℕm. ((inv(f) x ∈ ℕn) ∧ (↑(f (inv(f) x) =z x)) ∧ (∀[i:ℕn]. ¬↑(f i =z x) supposing i < inv(f) x))
⊢ inv(f) ∈ {g:ℕm ⟶ ℕn| Inj(ℕm;ℕn;g) ∧ (∀x:ℕm. ((f (g x)) = x ∈ ℤ))} 

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}].  \mforall{}[f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m|  Surj(\mBbbN{}n;\mBbbN{}m;f)\}  ].
    (inv(f)  \mmember{}  \{g:\mBbbN{}m  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}m;\mBbbN{}n;g)  \mwedge{}  (\mforall{}x:\mBbbN{}m.  ((f  (g  x))  =  x))\}  )


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  Unfold  `surject`  -1
  THEN  (Assert  \mforall{}x:\mBbbN{}m
                                ((inv(f)  x  \mmember{}  \mBbbN{}n)
                                \mwedge{}  (\muparrow{}(f  (inv(f)  x)  =\msubz{}  x))
                                \mwedge{}  (\mforall{}[i:\mBbbN{}n].  \mneg{}\muparrow{}(f  i  =\msubz{}  x)  supposing  i  <  inv(f)  x))  BY
                          (ParallelLast
                            THEN  ((InstLemma  `mu-bound-property+`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}n.(f  n  =\msubz{}  x)\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THENM  (RepUR  ``funinv``  0  THEN  Reduce  (-1)  THEN  Trivial)
                            )
                            THEN  Reduce  0
                            THEN  RW  assert\_pushdownC  0
                            THEN  Auto
                            THEN  ParallelLast
                            THEN  Auto)))

---

Home Index