---

Step * 1 of Lemma canonicalizable-baire-direct

.....wf..... 
λf,n. if (n) < (0)  then ⊥  else (f n) ∈ (ℕ ⟶ ℕ) ⟶ Base
BY
{ ((MemCD THENA Auto) THEN (PointwiseFunctionalityForEquality (-1) THENA Auto)) }

1
1. f : Base
2. f1 : Base
3. f = f1 ∈ (ℕ ⟶ ℕ)
⊢ (λn.if (n) < (0)  then ⊥  else (f n)) = (λn.if (n) < (0)  then ⊥  else (f1 n)) ∈ Base

---

Latex:

---

Latex:
.....wf..... 
\mlambda{}f,n.  if  (n)  <  (0)    then  \mbot{}    else  (f  n)  \mmember{}  (\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  Base


By

---

Latex:
((MemCD  THENA  Auto)  THEN  (PointwiseFunctionalityForEquality  (-1)  THENA  Auto))

---

Home Index