---

Step * of Lemma rneq-by-function

∀x,y,a,b:ℝ. ∀f:ℝ ⟶ ℝ.  (a ≠ b ⇒ (f[x] = a) ⇒ (f[y] = b) ⇒ (∀x,y:ℝ.  ((x = y) ⇒ (f[x] = f[y]))) ⇒ x ≠ y)
BY
{ (Auto
   THEN BLemma `real-weak-Markov`
   THEN Auto
   THEN (InstLemma `rneq-cases` [⌜f[x]⌝;⌜f[y]⌝;⌜f[z]⌝]⋅ THENA (Auto THEN RWO "7 8" 0 THEN Auto))
   THEN ParallelLast
   THEN (D 0 THENA Auto)
   THEN (FHyp (-4) [-1] THENA Auto)
   THEN (RWO  "-1" (-3) THENA Auto)
   THEN FLemma `rneq_irreflexivity` [-3]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x,y,a,b:\mBbbR{}.  \mforall{}f:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}.
    (a  \mneq{}  b  {}\mRightarrow{}  (f[x]  =  a)  {}\mRightarrow{}  (f[y]  =  b)  {}\mRightarrow{}  (\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y])))  {}\mRightarrow{}  x  \mneq{}  y)


By

---

Latex:
(Auto
  THEN  BLemma  `real-weak-Markov`
  THEN  Auto
  THEN  (InstLemma  `rneq-cases`  [\mkleeneopen{}f[x]\mkleeneclose{};\mkleeneopen{}f[y]\mkleeneclose{};\mkleeneopen{}f[z]\mkleeneclose{}]\mcdot{}  THENA  (Auto  THEN  RWO  "7  8"  0  THEN  Auto))
  THEN  ParallelLast
  THEN  (D  0  THENA  Auto)
  THEN  (FHyp  (-4)  [-1]  THENA  Auto)
  THEN  (RWO    "-1"  (-3)  THENA  Auto)
  THEN  FLemma  `rneq\_irreflexivity`  [-3]
  THEN  Auto)

---

Home Index