---

Step * 1 of Lemma face-of-intersection


1. v : ℚInterval
2. v1 : ℚInterval
3. v2 : ℚInterval
⊢ ((↑Inhabited(v2)) ∧ (↑Inhabited(v1))) ⇒ v ≤ v2 ⇒ v ≤ v1 ⇒ v ≤ v1 ⋂ v2
BY
{ ((∀h:hyp. D h 
    THEN RepUR ``rat-interval-face rat-point-interval`` 0
    THEN RepUR ``rat-interval-intersection inhabited-rat-interval`` 0)
   THEN RW assert_pushdownC 0
   THEN Auto) }

1
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)

---

Latex:

---

Latex:

1.  v  :  \mBbbQ{}Interval
2.  v1  :  \mBbbQ{}Interval
3.  v2  :  \mBbbQ{}Interval
\mvdash{}  ((\muparrow{}Inhabited(v2))  \mwedge{}  (\muparrow{}Inhabited(v1)))  {}\mRightarrow{}  v  \mleq{}  v2  {}\mRightarrow{}  v  \mleq{}  v1  {}\mRightarrow{}  v  \mleq{}  v1  \mcap{}  v2


By

---

Latex:
((\mforall{}h:hyp.  D  h 
    THEN  RepUR  ``rat-interval-face  rat-point-interval``  0
    THEN  RepUR  ``rat-interval-intersection  inhabited-rat-interval``  0)
  THEN  RW  assert\_pushdownC  0
  THEN  Auto)

---

Home Index