Step
*
of Lemma
ifun_subtype_1
∀[a,b,c:ℝ]. ((a ≤ c)
⇒ (c ≤ b)
⇒ ({f:[a, b] ⟶ℝ| ifun(f;[a, b])} ⊆r {f:[a, c] ⟶ℝ| ifun(f;[a, c])} ))
BY
{ (Auto THEN (D 0 THENA Auto) THEN D -1 THEN MemTypeCD THEN Auto) }
1
.....set predicate.....
1. a : ℝ
2. b : ℝ
3. c : ℝ
4. a ≤ c
5. c ≤ b
6. x : [a, b] ⟶ℝ
7. ifun(x;[a, b])
⊢ ifun(x;[a, c])
Latex:
Latex:
\mforall{}[a,b,c:\mBbbR{}].
((a \mleq{} c) {}\mRightarrow{} (c \mleq{} b) {}\mRightarrow{} (\{f:[a, b] {}\mrightarrow{}\mBbbR{}| ifun(f;[a, b])\} \msubseteq{}r \{f:[a, c] {}\mrightarrow{}\mBbbR{}| ifun(f;[a, c])\} ))
By
Latex:
(Auto THEN (D 0 THENA Auto) THEN D -1 THEN MemTypeCD THEN Auto)
Home
Index