---

Step * 1 1 of Lemma extensional-real-to-bool-constant


1. f : ℝ ⟶ 𝔹
2. ∀x,y:ℝ.  ((x = y) ⇒ f x = f y)
3. x : ℝ
4. y : ℝ
5. ¬f x = f y
6. x < y
⊢ False
BY
{ (RenameVar `a' 3
   THEN RenameVar `b' 4
   THEN (InstLemma `extensional-discrete-real-fun-is-constant` [⌜a⌝;⌜b⌝;⌜λ2x.if f x then 0 else 1 fi ⌝]⋅ THENA Auto)) }

1
1. f : ℝ ⟶ 𝔹
2. ∀x,y:ℝ.  ((x = y) ⇒ f x = f y)
3. a : ℝ
4. b : ℝ
5. ¬f a = f b
6. a < b
7. x : {x:ℝ| x ∈ [a, b]} 
8. y : {x:ℝ| x ∈ [a, b]} 
9. x = y
⊢ if f x then 0 else 1 fi  = if f y then 0 else 1 fi  ∈ ℤ

2
1. f : ℝ ⟶ 𝔹
2. ∀x,y:ℝ.  ((x = y) ⇒ f x = f y)
3. a : ℝ
4. b : ℝ
5. ¬f a = f b
6. a < b
7. ∀x,y:{x:ℝ| x ∈ [a, b]} .  (if f x then 0 else 1 fi  = if f y then 0 else 1 fi  ∈ ℤ)
⊢ False

---

Latex:

---

Latex:

1.  f  :  \mBbbR{}  {}\mrightarrow{}  \mBbbB{}
2.  \mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  f  x  =  f  y)
3.  x  :  \mBbbR{}
4.  y  :  \mBbbR{}
5.  \mneg{}f  x  =  f  y
6.  x  <  y
\mvdash{}  False


By

---

Latex:
(RenameVar  `a'  3
  THEN  RenameVar  `b'  4
  THEN  (InstLemma  `extensional-discrete-real-fun-is-constant`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.if  f  x  then  0  else  1  fi  \mkleeneclose{}
              ]\mcdot{}
              THENA  Auto
              ))

---

Home Index