---

Step * 1 of Lemma halfpi-interval-proper


1. i-finite((-(π/2), π/2))
⊢ -(π/2) < π/2
BY
{ (InstLemma `halfpi-positive` [] THEN DupHyp (-1) THEN nRAdd ⌜-(π/2)⌝ (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  i-finite((-(\mpi{}/2),  \mpi{}/2))
\mvdash{}  -(\mpi{}/2)  <  \mpi{}/2


By

---

Latex:
(InstLemma  `halfpi-positive`  []  THEN  DupHyp  (-1)  THEN  nRAdd  \mkleeneopen{}-(\mpi{}/2)\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)

---

Home Index