---

Step * of Lemma rfun_subtype_3

∀[a,b,c,d:ℝ].  ((a ≤ c) ⇒ (c ≤ d) ⇒ (d ≤ b) ⇒ ([a, b] ⟶ℝ ⊆r [c, d] ⟶ℝ))
BY
{ (Auto THEN (D 0 THENA Auto)) }

1
.....subterm..... T:t
1:n
1. a : ℝ
2. b : ℝ
3. c : ℝ
4. d : ℝ
5. a ≤ c
6. c ≤ d
7. d ≤ b
8. x : [a, b] ⟶ℝ
⊢ x ∈ [c, d] ⟶ℝ

---

Latex:

---

Latex:
\mforall{}[a,b,c,d:\mBbbR{}].    ((a  \mleq{}  c)  {}\mRightarrow{}  (c  \mleq{}  d)  {}\mRightarrow{}  (d  \mleq{}  b)  {}\mRightarrow{}  ([a,  b]  {}\mrightarrow{}\mBbbR{}  \msubseteq{}r  [c,  d]  {}\mrightarrow{}\mBbbR{}))


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto))

---

Home Index