---

Step * of Lemma separated-decider-not-extensional2

∀a,b:ℝ.  ((a < b) ⇒ (∀d:∀u:ℝ. ((a < u) ∨ (u < b)). (¬(∀x,y:ℝ.  ((x = y) ⇒ isl(d x) = isl(d y))))))
BY
{ (InstLemma `separated-decider-not-extensional` [] THEN RepeatFor 5 ((ParallelLast' THENA Auto))) }

1
1. a : ℝ
2. b : ℝ
3. a < b
4. d : ∀u:ℝ. ((a < u) ∨ (u < b))
5. ∀x,y:ℝ.  ((x = y) ⇒ isl(d x) = isl(d y))
⊢ ¬(∃x,y:ℝ. ((x = y) ∧ (↑isl(d x)) ∧ (↑isr(d y))))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    ((a  <  b)  {}\mRightarrow{}  (\mforall{}d:\mforall{}u:\mBbbR{}.  ((a  <  u)  \mvee{}  (u  <  b)).  (\mneg{}(\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  isl(d  x)  =  isl(d  y))))))


By

---

Latex:
(InstLemma  `separated-decider-not-extensional`  []  THEN  RepeatFor  5  ((ParallelLast'  THENA  Auto)))

---

Home Index