---

Step * of Lemma extensional-discrete-real-fun-is-constant

∀a,b:ℝ. ∀f:{x:ℝ| x ∈ [a, b]}  ⟶ ℤ.
  ∀x,y:{x:ℝ| x ∈ [a, b]} .  ((f x) = (f y) ∈ ℤ) supposing ∀x,y:{x:ℝ| x ∈ [a, b]} .  ((x = y) ⇒ ((f x) = (f y) ∈ ℤ))
BY
{ (InstLemma `real-fun-iff-continuous` []
   THEN RepeatFor 2 (ParallelLast')
   THEN Auto
   THEN DSetVars
   THEN All Reduce
   THEN (D 3 THENA Auto)
   THEN (Assert real-cont(λx.r(f x);a;b) BY
               (BHyp (-1)  THEN Auto THEN D 0 THEN Reduce 0 THEN Auto))
   THEN Thin (-2)) }

1
1. a : ℝ
2. b : ℝ
3. f : {x:ℝ| (a ≤ x) ∧ (x ≤ b)}  ⟶ ℤ
4. ∀x,y:{x:ℝ| (a ≤ x) ∧ (x ≤ b)} .  ((x = y) ⇒ ((f x) = (f y) ∈ ℤ))
5. x : ℝ
6. (a ≤ x) ∧ (x ≤ b)
7. y : ℝ
8. (a ≤ y) ∧ (y ≤ b)
9. real-cont(λx.r(f x);a;b)
⊢ (f x) = (f y) ∈ ℤ

---

Latex:

---

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


By

---

Latex:
(InstLemma  `real-fun-iff-continuous`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Auto
  THEN  DSetVars
  THEN  All  Reduce
  THEN  (D  3  THENA  Auto)
  THEN  (Assert  real-cont(\mlambda{}x.r(f  x);a;b)  BY
                          (BHyp  (-1)    THEN  Auto  THEN  D  0  THEN  Reduce  0  THEN  Auto))
  THEN  Thin  (-2))

---

Home Index