Step
*
1
of Lemma
bag-lub-property
1. T : Type
2. eq : EqDecider(T)@i
3. as : bag(T)@i
4. bs : bag(T)@i
5. sub-bag(T;as;bag-lub(eq;as;bs))
6. sub-bag(T;bs;bag-lub(eq;as;bs))
7. cs : bag(T)@i
8. ∀x:T. ((#x in as) ≤ (#x in cs))
9. ∀x:T. ((#x in bs) ≤ (#x in cs))
10. x : T@i
11. (#x in bs) ≤ (#x in cs)
12. (#x in as) ≤ (#x in cs)
⊢ imax((#x in as);(#x in bs)) ≤ (#x in cs)
BY
{ (BLemma `imax_lb` THEN Auto) }
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)@i
3. as : bag(T)@i
4. bs : bag(T)@i
5. sub-bag(T;as;bag-lub(eq;as;bs))
6. sub-bag(T;bs;bag-lub(eq;as;bs))
7. cs : bag(T)@i
8. \mforall{}x:T. ((\#x in as) \mleq{} (\#x in cs))
9. \mforall{}x:T. ((\#x in bs) \mleq{} (\#x in cs))
10. x : T@i
11. (\#x in bs) \mleq{} (\#x in cs)
12. (\#x in as) \mleq{} (\#x in cs)
\mvdash{} imax((\#x in as);(\#x in bs)) \mleq{} (\#x in cs)
By
Latex:
(BLemma `imax\_lb` THEN Auto)
Home
Index