---

Step * 1 of Lemma real-fun-implies-sfun-general


1. I : Interval
2. f : I ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))
4. x : {x:ℝ| x ∈ I} 
5. y : {x:ℝ| x ∈ I} 
6. f x ≠ f y
⊢ ∀z:ℝ. ((¬(z = x)) ∨ (¬(z = y)))
BY
{ (Assert ∀z:{x:ℝ| x ∈ I} . ((¬(z = x)) ∨ (¬(z = y))) BY
         (Auto
          THEN (InstLemma `rneq-cases` [⌜f x⌝;⌜f y⌝;⌜f z⌝]⋅ THENA Auto)
          THEN ParallelLast
          THEN D 0
          THEN Auto
          THEN (FHyp 3 [-1] THENA Auto)
          THEN (RWO  "-1" (-3) THENA Auto)
          THEN FLemma `rneq_irreflexivity` [-3]
          THEN Auto)) }

1
1. I : Interval
2. f : I ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))
4. x : {x:ℝ| x ∈ I} 
5. y : {x:ℝ| x ∈ I} 
6. f x ≠ f y
7. ∀z:{x:ℝ| x ∈ I} . ((¬(z = x)) ∨ (¬(z = y)))
⊢ ∀z:ℝ. ((¬(z = x)) ∨ (¬(z = y)))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f  :  I  {}\mrightarrow{}\mBbbR{}
3.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y)))
4.  x  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
5.  y  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
6.  f  x  \mneq{}  f  y
\mvdash{}  \mforall{}z:\mBbbR{}.  ((\mneg{}(z  =  x))  \mvee{}  (\mneg{}(z  =  y)))


By

---

Latex:
(Assert  \mforall{}z:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  ((\mneg{}(z  =  x))  \mvee{}  (\mneg{}(z  =  y)))  BY
              (Auto
                THEN  (InstLemma  `rneq-cases`  [\mkleeneopen{}f  x\mkleeneclose{};\mkleeneopen{}f  y\mkleeneclose{};\mkleeneopen{}f  z\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  ParallelLast
                THEN  D  0
                THEN  Auto
                THEN  (FHyp  3  [-1]  THENA  Auto)
                THEN  (RWO    "-1"  (-3)  THENA  Auto)
                THEN  FLemma  `rneq\_irreflexivity`  [-3]
                THEN  Auto))

---

Home Index