---

Step * 1 of Lemma finite-function


1. S : Type
2. T : S ⟶ Type
3. n : ℕ
4. S ~ ℕn
5. ∀s:S. ∃n:ℕ. T[s] ~ ℕn
6. f : s:S ⟶ ℕ
7. ∀s:S. T[s] ~ ℕf s
⊢ ∃n:ℕ. s:S ⟶ T[s] ~ ℕn
BY
{ ((FLemma `function_functionality_wrt_equipollent` [-1] THENA Auto) THEN (RWO "-1" 0 THENA Auto) THEN ThinVar `T') }

1
1. S : Type
2. n : ℕ
3. S ~ ℕn
4. f : s:S ⟶ ℕ
⊢ ∃n:ℕ. s:S ⟶ ℕf s ~ ℕn

---

Latex:

---

Latex:

1.  S  :  Type
2.  T  :  S  {}\mrightarrow{}  Type
3.  n  :  \mBbbN{}
4.  S  \msim{}  \mBbbN{}n
5.  \mforall{}s:S.  \mexists{}n:\mBbbN{}.  T[s]  \msim{}  \mBbbN{}n
6.  f  :  s:S  {}\mrightarrow{}  \mBbbN{}
7.  \mforall{}s:S.  T[s]  \msim{}  \mBbbN{}f  s
\mvdash{}  \mexists{}n:\mBbbN{}.  s:S  {}\mrightarrow{}  T[s]  \msim{}  \mBbbN{}n


By

---

Latex:
((FLemma  `function\_functionality\_wrt\_equipollent`  [-1]  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  ThinVar  `T')

---

Home Index