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