---

Step * of Lemma rfun_subtype_1

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

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

---

Latex:

---

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


By

---

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

---

Home Index