StevenXClontz’s avatarStevenXClontz’s Twitter Archive—№ 8,741

    1. Had a thought. @scratch is to Python as ??? is to @leanprover Parsons-Haden problems sort of scratch this itch (no pun intended, really), but where's my block-based proof assistant/verifier?
      oh my god twitter doesn’t include alt text from images in their API
      Permalink On twitter.com Twitter logo StevenXClontz’s avatar ❤️ 3 Favorites Mood -3 🙁
  1. …in reply to @StevenXClontz
    Yesterday I had the realization that some of my topology students are having issues with applying \exists and \forall appropriately when trying to prove regular+T0 imply T1. Why can't they drag a T1 block to a goal, be given the x,y they need to separate... 2/n
    On twitter.com Twitter logo StevenXClontz’s avatar ❤️ 1 Favorite Mood 0
    1. …in reply to @StevenXClontz
      then drag T0 to get two cases (it guarantees a nbhd U for x OR y, but we need both). Then drag "complement of open is closed" on U to get H, then drag regular into x,H to complete the proof.
      Permalink On twitter.com Twitter logo StevenXClontz’s avatar ❤️ 1 Favorite Mood -3 🙁