Step
*
1
1
of Lemma
inhabited-rat-cube-iff-point
1. [k] : ℕ
2. c : ℚCube(k)
3. ∀i:ℕk. (↑Inhabited(c i))
⊢ ∀i:ℕk. (((fst((c i))) ≤ (fst((c i)))) ∧ ((fst((c i))) ≤ (snd((c i)))))
BY
{ (ParallelLast THEN MoveToConcl (-1) THEN (GenConclTerm ⌜c i⌝⋅ THENA Auto)) }
1
1. [k] : ℕ
2. c : ℚCube(k)
3. ∀i:ℕk. (↑Inhabited(c i))
4. i : ℕk
5. v : ℚInterval
6. (c i) = v ∈ ℚInterval
⊢ (↑Inhabited(v))
⇒ (((fst(v)) ≤ (fst(v))) ∧ ((fst(v)) ≤ (snd(v))))
Latex:
Latex:
1. [k] : \mBbbN{}
2. c : \mBbbQ{}Cube(k)
3. \mforall{}i:\mBbbN{}k. (\muparrow{}Inhabited(c i))
\mvdash{} \mforall{}i:\mBbbN{}k. (((fst((c i))) \mleq{} (fst((c i)))) \mwedge{} ((fst((c i))) \mleq{} (snd((c i)))))
By
Latex:
(ParallelLast THEN MoveToConcl (-1) THEN (GenConclTerm \mkleeneopen{}c i\mkleeneclose{}\mcdot{} THENA Auto))
Home
Index