---

Step * of Lemma immediate-rc-face-implies

No Annotations
∀k:ℕ. ∀f,c:ℚCube(k).
  (0 < dim(c)
  ⇒ immediate-rc-face(k;f;c)
  ⇒ (∃i:ℕk
       ((dim(c i) = 1 ∈ ℤ)
       ∧ (∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ ((f j) = (c j) ∈ ℚInterval)))
       ∧ (((f i) = [fst((c i))] ∈ ℚInterval) ∨ ((f i) = [snd((c i))] ∈ ℚInterval)))))
BY
{ (Auto
   THEN Unfold `rat-cube-dimension` -2
   THEN SplitOnHypITE -2 
   THEN Auto
   THEN DupHyp (-1)
   THEN (RWO "assert-inhabited-rat-cube" (-1) THENA Auto)
   THEN D -3) }

1
1. k : ℕ
2. f : ℚCube(k)
3. c : ℚCube(k)
4. 0 < Σ(dim(c i) | i < k)
5. f ≤ c
6. dim(f) = (dim(c) - 1) ∈ ℤ
7. ↑Inhabited(c)
8. ∀i:ℕk. (↑Inhabited(c i))
⊢ ∃i:ℕk
   ((dim(c i) = 1 ∈ ℤ)
   ∧ (∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ ((f j) = (c j) ∈ ℚInterval)))
   ∧ (((f i) = [fst((c i))] ∈ ℚInterval) ∨ ((f i) = [snd((c i))] ∈ ℚInterval)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}k:\mBbbN{}.  \mforall{}f,c:\mBbbQ{}Cube(k).
    (0  <  dim(c)
    {}\mRightarrow{}  immediate-rc-face(k;f;c)
    {}\mRightarrow{}  (\mexists{}i:\mBbbN{}k
              ((dim(c  i)  =  1)
              \mwedge{}  (\mforall{}j:\mBbbN{}k.  ((\mneg{}(j  =  i))  {}\mRightarrow{}  ((f  j)  =  (c  j))))
              \mwedge{}  (((f  i)  =  [fst((c  i))])  \mvee{}  ((f  i)  =  [snd((c  i))])))))


By

---

Latex:
(Auto
  THEN  Unfold  `rat-cube-dimension`  -2
  THEN  SplitOnHypITE  -2 
  THEN  Auto
  THEN  DupHyp  (-1)
  THEN  (RWO  "assert-inhabited-rat-cube"  (-1)  THENA  Auto)
  THEN  D  -3)

---

Home Index