org/robotone-opensets.org

   1 #+TITLE:     ROBOTONE - If $A$ and $B$ are open sets, then $A\cap B$ is also open
   2 #+AUTHOR:    Brought to you by the letters δ, η, and θ.
   3 #+DATE:      May 16, 2017
   4 #+DESCRIPTION: IATC transcription of a short formal proof
   5 #+KEYWORDS: mathematical argumentation
   6 #+LANGUAGE: en
   7 #+OPTIONS: H:3 num:t toc:t \n:nil @:t ::t |:t ^:nil -:t f:t *:t <:t
   8 #+OPTIONS: TeX:t LaTeX:nil skip:nil d:nil todo:t pri:nil tags:not-in-toc
   9 #+INFOJS_OPT: view:nil toc:nil ltoc:t mouse:underline buttons:0 path:http://orgmode.org/org-info.js
  10 #+EXPORT_SELECT_TAGS: export
  11 #+EXPORT_EXCLUDE_TAGS: noexport
  12 #+LINK_UP:
  13 #+LINK_HOME:
  14 #+HTML_HEAD: <link rel="stylesheet" type="text/css" href="http://metameso.org/~joe/solarized-css/build/solarized-light.css" />
  15 #+STARTUP: showeverything
  16
  17 * "If $A$ and $B$ are open sets, then $A\cap B$ is also open"
  18
  19 If $A$ and $B$ are open sets, then $A\cap B$ is also open.
  20
  21 #+BEGIN_SRC
  22 IATC> perf[assert](meta[goal](rel[implies](rel[conjunction](H1: A is open,H2: B is open), T1: A∩B is open)))
  23 IATC> perf[suggest](meta[strategy](expand definitions: expand pre-universal target))
  24 IATC> rel[equivalent_to](T1,T2:forall x.(x in A∩B => exists δ. (forall y. (d(x,y)<δ => y in A∩B))))
  25 #+END_SRC
  26
  27 Let $x$ be an element of $A\cap B$.
  28
  29 #+BEGIN_SRC
  30 IATC> perf[suggest](meta[strategy](introduce concrete variables: apply 'let' trick and move premise of universal-conditional target T2 above the line, i.e., suppose the antecedent is not vacuous)
  31 IATC> rel[add assumption](introduce concrete variables,H3:x in A∩B)
  32 IATC> rel[replace with](T2,T3:exists δ. (forall y.(d(x,y)<δ => y in A∩B)))
  33 #+END_SRC
  34
  35 Then $x\in A$ and $x\in B$.
  36
  37 #+BEGIN_SRC
  38 perf[assert](rel[equivalent to](H3,rel[conjunction](H4: x in A, H5: x in B)))
  39 rel[by inference rule](equivalent to,quantifier-free expansion of hypothesis H3)
  40 #+END_SRC
  41
  42 Therefore, since $A$ is open, there exists $\eta>0$
  43 such that $u\in A$ whenever $d(x,u)<\eta$.
  44
  45 #+BEGIN_SRC
  46 perf[suggest](meta[strategy](expand definitions))
  47 rel[implies](rel[conjunction](H1,H4),H6: forall u.(d(x,u)<η[x]=>u in A))
  48 rel[by inference rule](implies,forwards reasoning using H1 with H4)
  49 #+END_SRC
  50
  51 Since $B$ is open, there exists $\theta>0$
  52 such that $v\in B$ whenever $d(x,v)<\theta$.
  53
  54 #+BEGIN_SRC
  55 perf[suggest](meta[strategy](expand definitions))
  56 rel[implies](rel[conjunction](H2,H5),H6: forall v.(d(x,v)<θ[x]=>v in B))
  57 rel[by inference rule](implies,forwards reasoning using H2 with H5)
  58 #+END_SRC
  59
  60 We would like to find $\delta>0$ such that
  61 $y\in A\cap B$ whenever $d(x,y)<\delta$.
  62
  63 #+BEGIN_SRC
  64 rel[implies](H8: d(x,y)<δ,T4:y in A∩B)
  65 perf[suggest](meta[strategy](sufficient to show, there exists some δ with this property: implies))
  66 rel[replace with](T3,there exists some δ with this property)
  67 #+END_SRC
  68
  69 But $y\in A\cap B$ if and only if $y\in A$ and $y\in B$.
  70
  71 #+BEGIN_SRC
  72 perf[assert](rel[equivalent to](T4,rel[conjunction](T5:y in A,T6:y in B)))
  73 rel[by inference rule](equivalent to,quantifier free expansion of target T4)
  74 #+END_SRC
  75
  76 We know that $y\in A$ whenever $d(x,y)<\eta$.
  77
  78 #+BEGIN_SRC
  79 perf[assert](rel[implies](T7:d(x,y)<η[x],T5)
  80 rel[by inference rule](implies, backwards reasoning using H6 with T5)
  81 #+END_SRC
  82
  83 And that $y\in B$ whenever $d(x,y)<\theta$.
  84
  85 #+BEGIN_SRC
  86 perf[assert](rel[implies](T8:d(x,y)<θ[x],T6)
  87 rel[by inference rule](implies, backwards reasoning using H7 with T6)
  88 #+END_SRC
  89
  90 Assume now that $d(x,y)<\delta$.
  91
  92 #+BEGIN_SRC
  93 perf[suggest](meta[strategy](consider concrete instances where this property holds,H8))
  94 perf[assert](d(x,y)<δ)
  95 #+END_SRC
  96
  97 Then $d(x,y) < \eta$ if $\delta\leq\eta$.
  98
  99 #+BEGIN_SRC
 100 perf[assert](meta[strategy](we can now obtain this desired result with this selection,T7))
 101 perf[assert](d(x,y<δ and δ <= η implies d(x,y) < η))
 102 rel[by inference rule](we can now obtain this desired result with this selection, backwards reasoning using library result transitivity with T7 and H8)
 103 #+END_SRC
 104
 105 And $d(x,y) < \theta$ if $\delta\leq\theta$.
 106
 107 #+BEGIN_SRC
 108 perf[assert](meta[strategy](we can now obtain this desired result with this selection,T7))
 109 perf[assert](d(x,y<δ and δ <= θ implies d(x,y) < θ))
 110 rel[by inference rule](we can now obtain this desired result with this selection, backwards reasoning using library result transitivity with T8 and H8)
 111 #+END_SRC
 112
 113 We may therefore take $\delta = \min(\eta,\theta) and we are done.
 114
 115 #+BEGIN_SRC
 116 perf[assert](rel[has property](δ=min(η, θ),d(x,y)<δ => y in A∩B))
 117 perf[assert](we have found a δ with the condition we need to satisfy, T3)
 118 #+END_SRC