---

Step * of Lemma weak-continuity-bool-bool

No Annotations
weak-continuity(𝔹;𝔹)
BY
{ ((D 0 THENA Auto)
   THEN (InstLemma strong-continuity2-implies-weak-skolem-cantor [⌜F⌝]⋅ THENA Auto)
   THEN (ExRepD THENA Auto)) }

1
1. F : (ℕ ⟶ 𝔹) ⟶ 𝔹
2. ⇃(∃M:(ℕ ⟶ 𝔹) ⟶ ℕ. ∀f,g:ℕ ⟶ 𝔹.  ((f = g ∈ (ℕM f ⟶ 𝔹)) ⇒ F f = F g))
3. f : ℕ ⟶ 𝔹
⊢ ↓∃n:ℕ. ∀g:ℕ ⟶ 𝔹. ((∀i:ℕn. f i = g i) ⇒ F f = F g)

---

Latex:

---

Latex:
No  Annotations
weak-continuity(\mBbbB{};\mBbbB{})


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (InstLemma  strong-continuity2-implies-weak-skolem-cantor  [\mkleeneopen{}F\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (ExRepD  THENA  Auto))

---

Home Index