Step
*
of Lemma
rat-cube-face-dimension-equal
∀[k:ℕ]. ∀[c:ℚCube(k)]. ∀f:ℚCube(k). (f = c ∈ ℚCube(k)) supposing ((dim(f) = dim(c) ∈ ℤ) and f ≤ c) supposing ↑Inhabited\000C(c)
BY
{ (Auto
THEN (InstLemma `inhabited-rat-cube-face` [⌜k⌝;⌜c⌝;⌜f⌝]⋅ THENA Auto)
THEN (All (RWO "assert-inhabited-rat-cube") THENA Auto)) }
1
1. k : ℕ
2. c : ℚCube(k)
3. ∀i:ℕk. (↑Inhabited(c i))
4. f : ℚCube(k)
5. f ≤ c
6. dim(f) = dim(c) ∈ ℤ
7. ∀i:ℕk. (↑Inhabited(f i))
⊢ f = c ∈ ℚCube(k)
Latex:
Latex:
\mforall{}[k:\mBbbN{}]. \mforall{}[c:\mBbbQ{}Cube(k)]. \mforall{}f:\mBbbQ{}Cube(k). (f = c) supposing ((dim(f) = dim(c)) and f \mleq{} c) supposing \muparrow{}Inha\000Cbited(c)
By
Latex:
(Auto
THEN (InstLemma `inhabited-rat-cube-face` [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (All (RWO "assert-inhabited-rat-cube") THENA Auto))
Home
Index