---

Step * of Lemma rat-point-in-intersection

No Annotations
∀[k:ℕ]. ∀[x:ℕk ⟶ ℚ]. ∀[c,d:ℚCube(k)].
  uiff(rat-point-in-cube(k;x;c ⋂ d);rat-point-in-cube(k;x;c) ∧ rat-point-in-cube(k;x;d))
BY
{ (Auto THEN RepeatFor 2 (ParallelLast)) }

1
1. k : ℕ
2. x : ℕk ⟶ ℚ
3. c : ℚCube(k)
4. d : ℚCube(k)
5. ∀i:ℕk. (((fst((c ⋂ d i))) ≤ (x i)) ∧ ((x i) ≤ (snd((c ⋂ d i)))))
6. i : ℕk
7. ((fst((c ⋂ d i))) ≤ (x i)) ∧ ((x i) ≤ (snd((c ⋂ d i))))
⊢ ((fst((c i))) ≤ (x i)) ∧ ((x i) ≤ (snd((c i))))

2
1. k : ℕ
2. x : ℕk ⟶ ℚ
3. c : ℚCube(k)
4. d : ℚCube(k)
5. ∀i:ℕk. (((fst((c ⋂ d i))) ≤ (x i)) ∧ ((x i) ≤ (snd((c ⋂ d i)))))
6. i : ℕk
7. ((fst((c ⋂ d i))) ≤ (x i)) ∧ ((x i) ≤ (snd((c ⋂ d i))))
⊢ ((fst((d i))) ≤ (x i)) ∧ ((x i) ≤ (snd((d i))))

3
1. k : ℕ
2. x : ℕk ⟶ ℚ
3. c : ℚCube(k)
4. d : ℚCube(k)
5. rat-point-in-cube(k;x;c)
6. ∀i:ℕk. (((fst((d i))) ≤ (x i)) ∧ ((x i) ≤ (snd((d i)))))
7. i : ℕk
8. ((fst((d i))) ≤ (x i)) ∧ ((x i) ≤ (snd((d i))))
⊢ ((fst((c ⋂ d i))) ≤ (x i)) ∧ ((x i) ≤ (snd((c ⋂ d i))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[k:\mBbbN{}].  \mforall{}[x:\mBbbN{}k  {}\mrightarrow{}  \mBbbQ{}].  \mforall{}[c,d:\mBbbQ{}Cube(k)].
    uiff(rat-point-in-cube(k;x;c  \mcap{}  d);rat-point-in-cube(k;x;c)  \mwedge{}  rat-point-in-cube(k;x;d))


By

---

Latex:
(Auto  THEN  RepeatFor  2  (ParallelLast))

---

Home Index