---

Step * of Lemma continuous-monotone-co-value

ContinuousMonotone(T.atomic-values() ⋃ (T × T) ⋃ (T + T))
BY
{ ((D 0 THEN Auto) THEN Repeat ((BLemma `strong-continuous-b-union` THEN Auto)) THEN D 0 THEN Auto) }

1
1. T : Type
2. S : Type
3. T × T ⋂ S + S
⊢ False

2
1. T : Type
2. S : Type
3. atomic-values() ⋂ (S × S) ⋃ (S + S)
⊢ False

---

Latex:

---

Latex:
ContinuousMonotone(T.atomic-values()  \mcup{}  (T  \mtimes{}  T)  \mcup{}  (T  +  T))


By

---

Latex:
((D  0  THEN  Auto)  THEN  Repeat  ((BLemma  `strong-continuous-b-union`  THEN  Auto))  THEN  D  0  THEN  Auto)

---

Home Index