---

Step * of Lemma compose-strict-inc

∀s,f:StrictInc.  (s o f ∈ StrictInc)
BY
{ (Auto THEN D 1 THEN D -1 THEN MemTypeCD THEN Auto) }

1
1. s : ℕ ⟶ ℕ@i
2. ∀j:ℕ. ∀i:ℕj.  s i < s j@i
3. f : ℕ ⟶ ℕ@i
4. ∀j:ℕ. ∀i:ℕj.  f i < f j@i
5. j : ℕ@i
6. i : ℕj@i
⊢ (s o f) i < (s o f) j

---

Latex:

---

Latex:
\mforall{}s,f:StrictInc.    (s  o  f  \mmember{}  StrictInc)


By

---

Latex:
(Auto  THEN  D  1  THEN  D  -1  THEN  MemTypeCD  THEN  Auto)

---

Home Index