---

Step * 1 1 1 of Lemma face-of-intersection


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)
BY
{ (Subst' qmax(v4;v3) = v4 ∈ ℚ 0 THEN EAuto 1) }

---

Latex:

---

Latex:

1.  v4  :  \mBbbQ{}
2.  v6  :  \mBbbQ{}
3.  v3  :  \mBbbQ{}
4.  v3  \mleq{}  v4
5.  v4  \mleq{}  v6
6.  v4  =  v4
\mvdash{}  (<v4,  v4>  =  <qmax(v4;v3),  qmax(v4;v3)>)
\mvee{}  (<v4,  v4>  =  <qmin(v6;v4),  qmin(v6;v4)>)
\mvee{}  (<v4,  v4>  =  <qmax(v4;v3),  qmin(v6;v4)>)


By

---

Latex:
(Subst'  qmax(v4;v3)  =  v4  0  THEN  EAuto  1)

---

Home Index