---

Step * 1 of Lemma omral_scale_dom_bound


1. g : OCMon
2. r : CDRng
3. bound : |g|
4. k : |g|
5. v : |r|
6. ps : (|g| × |r|) List
7. ↑(∀bx(:|g|) ∈ map(λz.(fst(z));ps)
        (x <b bound))
⊢ ↑(∀bx(:|g|) ∈ map(λz.(fst(z));ps)
       ((k * x) <b (k * bound)))
BY
{ % This is so ugly! (ball_char wants to match a set_car, 
  not a grp_car) % 
((Assert |g| = |(g↓oset)| ∈ Type THENA Reduce 0) THEN Auto) 
THEN ((OnMCls [0;7] (RewriteWith [-1] ``ball_char``)) THENA Auto) 
THEN Thin (-1) }

1
1. g : OCMon
2. r : CDRng
3. bound : |g|
4. k : |g|
5. v : |r|
6. ps : (|g| × |r|) List
7. ∀x:|(g↓oset)|. ((↑(x ∈b map(λz.(fst(z));ps))) ⇒ (↑(x <b bound)))
⊢ ∀x:|(g↓oset)|. ((↑(x ∈b map(λz.(fst(z));ps))) ⇒ (↑((k * x) <b (k * bound))))

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  bound  :  |g|
4.  k  :  |g|
5.  v  :  |r|
6.  ps  :  (|g|  \mtimes{}  |r|)  List
7.  \muparrow{}(\mforall{}\msubb{}x(:|g|)  \mmember{}  map(\mlambda{}z.(fst(z));ps)
                (x  <\msubb{}  bound))
\mvdash{}  \muparrow{}(\mforall{}\msubb{}x(:|g|)  \mmember{}  map(\mlambda{}z.(fst(z));ps)
              ((k  *  x)  <\msubb{}  (k  *  bound)))


By

---

Latex:
\%  This  is  so  ugly!  (ball\_char  wants  to  match  a  set\_car, 
    not  a  grp\_car)  \% 
((Assert  |g|  =  |(g\mdownarrow{}oset)|  THENA  Reduce  0)  THEN  Auto) 
THEN  ((OnMCls  [0;7]  (RewriteWith  [-1]  ``ball\_char``))  THENA  Auto) 
THEN  Thin  (-1)

---

Home Index