Step * of Lemma r2-nontrivial

No Annotations
a:ℝ^2. (∃b:ℝ^2 [(d(a;a) < d(a;b))])
BY
((InstLemma `rv-sep-exists` [⌜2⌝]⋅ THEN Auto) THEN ParallelLast THEN -1) }

1
1. : ℝ^2
2. : ℝ^2
3. a ≠ b
⊢ ∃b:ℝ^2 [(d(a;a) < d(a;b))]


Latex:


Latex:
No  Annotations
\mexists{}a:\mBbbR{}\^{}2.  (\mexists{}b:\mBbbR{}\^{}2  [(d(a;a)  <  d(a;b))])


By


Latex:
((InstLemma  `rv-sep-exists`  [\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  ParallelLast  THEN  D  -1)




Home Index