---

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


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index