---

Step * 1 of Lemma unsquashed-weak-continuity-base-false


1. MC : F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base ⟶ ℕ ⟶ ℕ ⋂ Base ⟶ ℕ
2. ∀F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base. ∀a,b:ℕ ⟶ ℕ ⋂ Base.  ((∀i:ℕMC F a. ((a i) = (b i) ∈ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ))
⊢ False
BY
{ TACTIC:(PointwiseFunctionality 1
          THEN Auto
          THEN Unhide
          THEN RenameVar `MC' 1
          THEN (Assert MC ∈ F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base ⟶ ℕ ⟶ ℕ ⋂ Base ⟶ ℕ BY
                      Eq)
          THEN RepeatFor 2 (Thin (-3))
          THEN PromoteHyp (-1) 2) }

1
1. MC : Base
2. MC ∈ F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base ⟶ ℕ ⟶ ℕ ⋂ Base ⟶ ℕ
3. ∀F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base. ∀a@0,b:ℕ ⟶ ℕ ⋂ Base.  ((∀i:ℕMC F a@0. ((a@0 i) = (b i) ∈ ℕ)) ⇒ ((F a@0) = (F b) ∈ ℕ))
⊢ False

---

Latex:

---

Latex:

1.  MC  :  F:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base  {}\mrightarrow{}  \mBbbN{}
2.  \mforall{}F:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base.  \mforall{}a,b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base.
          ((\mforall{}i:\mBbbN{}MC  F  a.  ((a  i)  =  (b  i)))  {}\mRightarrow{}  ((F  a)  =  (F  b)))
\mvdash{}  False


By

---

Latex:
TACTIC:(PointwiseFunctionality  1
                THEN  Auto
                THEN  Unhide
                THEN  RenameVar  `MC'  1
                THEN  (Assert  MC  \mmember{}  F:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base  {}\mrightarrow{}  \mBbbN{}  BY
                                        Eq)
                THEN  RepeatFor  2  (Thin  (-3))
                THEN  PromoteHyp  (-1)  2)

---

Home Index