---

Step * of Lemma canonical-function_wf

∀X:{X:Type| X ⊆r Base} . ∀f:ℕ ⟶ X.  (canonical-function(f) ∈ {g:Base| g = f ∈ (ℕ ⟶ X)} )
BY
{ TACTIC:((UnivCD THENA Auto) THEN D 1 THEN Assert ⌜canonical-function(f) ∈ Base⌝⋅) }

1
.....assertion..... 
1. X : Type
2. X ⊆r Base
3. f : ℕ ⟶ X
⊢ canonical-function(f) ∈ Base

2
1. X : Type
2. X ⊆r Base
3. f : ℕ ⟶ X
4. canonical-function(f) ∈ Base
⊢ canonical-function(f) ∈ {g:Base| g = f ∈ (ℕ ⟶ X)} 

---

Latex:

---

Latex:
\mforall{}X:\{X:Type|  X  \msubseteq{}r  Base\}  .  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  X.    (canonical-function(f)  \mmember{}  \{g:Base|  g  =  f\}  )


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)  THEN  D  1  THEN  Assert  \mkleeneopen{}canonical-function(f)  \mmember{}  Base\mkleeneclose{}\mcdot{})

---

Home Index