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