---

Step * of Lemma bar-diverges-iff

∀[T:Type]. ∀[x:bar-base(T)].  (x↑ ⇐⇒ ∀[a:T]. (¬x↓a))
BY
{ (Auto THEN Try (((D 0 THENA Auto) THEN FLemma `bar-converges-not-diverges` [-1] THEN Auto))) }

1
1. T : Type
2. x : bar-base(T)
3. ∀[a:T]. (¬x↓a)
⊢ x↑

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:bar-base(T)].    (x\muparrow{}  \mLeftarrow{}{}\mRightarrow{}  \mforall{}[a:T].  (\mneg{}x\mdownarrow{}a))


By

---

Latex:
(Auto  THEN  Try  (((D  0  THENA  Auto)  THEN  FLemma  `bar-converges-not-diverges`  [-1]  THEN  Auto)))

---

Home Index