---

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


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) ∈ ℤ
BY
{ ((D -1 With ⌜2⌝  THENA Auto) THEN Reduce -1 THEN ExRepD THEN Auto) }

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
7. x ≤ b
8. y : ℝ
9. a ≤ y
10. y ≤ b
11. d : {d:ℝ| r0 < d} 
12. ∀x,y:{x:ℝ| (a ≤ x) ∧ (x ≤ b)} .  ((|x - y| ≤ d) ⇒ (|r(f x) - r(f y)| ≤ (r1/r(2))))
⊢ (f x) = (f y) ∈ ℤ

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  f  :  \{x:\mBbbR{}|  (a  \mleq{}  x)  \mwedge{}  (x  \mleq{}  b)\}    {}\mrightarrow{}  \mBbbZ{}
4.  \mforall{}x,y:\{x:\mBbbR{}|  (a  \mleq{}  x)  \mwedge{}  (x  \mleq{}  b)\}  .    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y)))
5.  x  :  \mBbbR{}
6.  (a  \mleq{}  x)  \mwedge{}  (x  \mleq{}  b)
7.  y  :  \mBbbR{}
8.  (a  \mleq{}  y)  \mwedge{}  (y  \mleq{}  b)
9.  real-cont(\mlambda{}x.r(f  x);a;b)
\mvdash{}  (f  x)  =  (f  y)


By

---

Latex:
((D  -1  With  \mkleeneopen{}2\mkleeneclose{}    THENA  Auto)  THEN  Reduce  -1  THEN  ExRepD  THEN  Auto)

---

Home Index