---

Step * 1 1 of Lemma face-of-intersection


1. v7 : ℚ
2. v8 : ℚ
3. v5 : ℚ
4. v6 : ℚ
5. v3 : ℚ
6. v4 : ℚ
7. v3 ≤ v4
8. v5 ≤ v6
9. (<v7, v8> = <v3, v3> ∈ ℚInterval) ∨ (<v7, v8> = <v4, v4> ∈ ℚInterval) ∨ (<v7, v8> = <v3, v4> ∈ ℚInterval)
10. (<v7, v8> = <v5, v5> ∈ ℚInterval) ∨ (<v7, v8> = <v6, v6> ∈ ℚInterval) ∨ (<v7, v8> = <v5, v6> ∈ ℚInterval)
⊢ (<v7, v8> = <qmax(v5;v3), qmax(v5;v3)> ∈ ℚInterval)
∨ (<v7, v8> = <qmin(v6;v4), qmin(v6;v4)> ∈ ℚInterval)
∨ (<v7, v8> = <qmax(v5;v3), qmin(v6;v4)> ∈ ℚInterval)
BY
{ ((SplitOrHyps THEN ∀h:hyp. (EqHD h THENA Auto) )
   THEN All Reduce
   THEN RationalElim ⌜v7⌝⋅
   THEN RationalElim ⌜v8⌝⋅
   THEN Try (RationalElim ⌜v6⌝⋅)
   THEN Try (RationalElim ⌜v5⌝⋅)
   THEN (RWW "qmax-idempotent qmin-idempotent" 0 THENA Auto)
   THEN Auto) }

1
1. v4 : ℚ
2. v6 : ℚ
3. v3 : ℚ
4. v3 ≤ v4
5. v4 ≤ v6
6. v4 = v4 ∈ ℚ
⊢ (<v4, v4> = <qmax(v4;v3), qmax(v4;v3)> ∈ ℚInterval)
∨ (<v4, v4> = <qmin(v6;v4), qmin(v6;v4)> ∈ ℚInterval)
∨ (<v4, v4> = <qmax(v4;v3), qmin(v6;v4)> ∈ ℚInterval)

2
1. v3 : ℚ
2. v5 : ℚ
3. v4 : ℚ
4. v3 ≤ v4
5. v5 ≤ v3
6. v3 = v3 ∈ ℚ
⊢ (<v3, v3> = <qmax(v5;v3), qmax(v5;v3)> ∈ ℚInterval)
∨ (<v3, v3> = <qmin(v3;v4), qmin(v3;v4)> ∈ ℚInterval)
∨ (<v3, v3> = <qmax(v5;v3), qmin(v3;v4)> ∈ ℚInterval)

3
1. v3 : ℚ
2. v4 : ℚ
3. v5 : ℚ
4. v3 ≤ v4
5. v5 ≤ v3
6. v4 = v3 ∈ ℚ
⊢ (<v3, v4> = <qmax(v5;v3), qmax(v5;v3)> ∈ ℚInterval)
∨ (<v3, v4> = <qmin(v3;v4), qmin(v3;v4)> ∈ ℚInterval)
∨ (<v3, v4> = <qmax(v5;v3), qmin(v3;v4)> ∈ ℚInterval)

---

Latex:

---

Latex:

1.  v7  :  \mBbbQ{}
2.  v8  :  \mBbbQ{}
3.  v5  :  \mBbbQ{}
4.  v6  :  \mBbbQ{}
5.  v3  :  \mBbbQ{}
6.  v4  :  \mBbbQ{}
7.  v3  \mleq{}  v4
8.  v5  \mleq{}  v6
9.  (<v7,  v8>  =  <v3,  v3>)  \mvee{}  (<v7,  v8>  =  <v4,  v4>)  \mvee{}  (<v7,  v8>  =  <v3,  v4>)
10.  (<v7,  v8>  =  <v5,  v5>)  \mvee{}  (<v7,  v8>  =  <v6,  v6>)  \mvee{}  (<v7,  v8>  =  <v5,  v6>)
\mvdash{}  (<v7,  v8>  =  <qmax(v5;v3),  qmax(v5;v3)>)
\mvee{}  (<v7,  v8>  =  <qmin(v6;v4),  qmin(v6;v4)>)
\mvee{}  (<v7,  v8>  =  <qmax(v5;v3),  qmin(v6;v4)>)


By

---

Latex:
((SplitOrHyps  THEN  \mforall{}h:hyp.  (EqHD  h  THENA  Auto)  )
  THEN  All  Reduce
  THEN  RationalElim  \mkleeneopen{}v7\mkleeneclose{}\mcdot{}
  THEN  RationalElim  \mkleeneopen{}v8\mkleeneclose{}\mcdot{}
  THEN  Try  (RationalElim  \mkleeneopen{}v6\mkleeneclose{}\mcdot{})
  THEN  Try  (RationalElim  \mkleeneopen{}v5\mkleeneclose{}\mcdot{})
  THEN  (RWW  "qmax-idempotent  qmin-idempotent"  0  THENA  Auto)
  THEN  Auto)

---

Home Index