---

Step * of Lemma compatible-rat-intervals-iff

∀I,J:ℚInterval.
  ((↑Inhabited(I))
  ⇒ (↑Inhabited(J))
  ⇒ (↑Inhabited(I ⋂ J))
  ⇒ (I ⋂ J ≤ I ∧ I ⋂ J ≤ J ⇐⇒ (I = J ∈ ℚInterval) ∨ ((snd(I)) = (fst(J)) ∈ ℚ) ∨ ((snd(J)) = (fst(I)) ∈ ℚ)))
BY
{ (RepeatFor 2 (((D 0 THENA Auto) THEN D -1))
   THEN RepUR ``rat-interval-intersection inhabited-rat-interval`` 0
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN RepUR ``rat-interval-face`` 0
   THEN Auto) }

1
1. I1 : ℚ
2. I2 : ℚ
3. J1 : ℚ
4. J2 : ℚ
5. I1 ≤ I2
6. J1 ≤ J2
7. qmax(I1;J1) ≤ qmin(I2;J2)
8. (<qmax(I1;J1), qmin(I2;J2)> = [I1] ∈ ℚInterval)
∨ (<qmax(I1;J1), qmin(I2;J2)> = [I2] ∈ ℚInterval)
∨ (<qmax(I1;J1), qmin(I2;J2)> = <I1, I2> ∈ ℚInterval)
9. (<qmax(I1;J1), qmin(I2;J2)> = [J1] ∈ ℚInterval)
∨ (<qmax(I1;J1), qmin(I2;J2)> = [J2] ∈ ℚInterval)
∨ (<qmax(I1;J1), qmin(I2;J2)> = <J1, J2> ∈ ℚInterval)
⊢ (<I1, I2> = <J1, J2> ∈ ℚInterval) ∨ (I2 = J1 ∈ ℚ) ∨ (J2 = I1 ∈ ℚ)

2
1. I1 : ℚ
2. I2 : ℚ
3. J1 : ℚ
4. J2 : ℚ
5. I1 ≤ I2
6. J1 ≤ J2
7. qmax(I1;J1) ≤ qmin(I2;J2)
8. (<I1, I2> = <J1, J2> ∈ ℚInterval) ∨ (I2 = J1 ∈ ℚ) ∨ (J2 = I1 ∈ ℚ)
⊢ (<qmax(I1;J1), qmin(I2;J2)> = [I1] ∈ ℚInterval)
∨ (<qmax(I1;J1), qmin(I2;J2)> = [I2] ∈ ℚInterval)
∨ (<qmax(I1;J1), qmin(I2;J2)> = <I1, I2> ∈ ℚInterval)

3
1. I1 : ℚ
2. I2 : ℚ
3. J1 : ℚ
4. J2 : ℚ
5. I1 ≤ I2
6. J1 ≤ J2
7. qmax(I1;J1) ≤ qmin(I2;J2)
8. (<I1, I2> = <J1, J2> ∈ ℚInterval) ∨ (I2 = J1 ∈ ℚ) ∨ (J2 = I1 ∈ ℚ)
⊢ (<qmax(I1;J1), qmin(I2;J2)> = [J1] ∈ ℚInterval)
∨ (<qmax(I1;J1), qmin(I2;J2)> = [J2] ∈ ℚInterval)
∨ (<qmax(I1;J1), qmin(I2;J2)> = <J1, J2> ∈ ℚInterval)

---

Latex:

---

Latex:
\mforall{}I,J:\mBbbQ{}Interval.
    ((\muparrow{}Inhabited(I))
    {}\mRightarrow{}  (\muparrow{}Inhabited(J))
    {}\mRightarrow{}  (\muparrow{}Inhabited(I  \mcap{}  J))
    {}\mRightarrow{}  (I  \mcap{}  J  \mleq{}  I  \mwedge{}  I  \mcap{}  J  \mleq{}  J  \mLeftarrow{}{}\mRightarrow{}  (I  =  J)  \mvee{}  ((snd(I))  =  (fst(J)))  \mvee{}  ((snd(J))  =  (fst(I)))))


By

---

Latex:
(RepeatFor  2  (((D  0  THENA  Auto)  THEN  D  -1))
  THEN  RepUR  ``rat-interval-intersection  inhabited-rat-interval``  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  RepUR  ``rat-interval-face``  0
  THEN  Auto)

---

Home Index