equal
deleted
inserted
replaced
11 lemma le_left_mono: "x \<le> y \<Longrightarrow> y \<le> a \<longrightarrow> x \<le> (a::'a::preorder)" |
11 lemma le_left_mono: "x \<le> y \<Longrightarrow> y \<le> a \<longrightarrow> x \<le> (a::'a::preorder)" |
12 by (auto intro: order_trans) |
12 by (auto intro: order_trans) |
13 |
13 |
14 lemma ball_trans: |
14 lemma ball_trans: |
15 assumes "y \<in> ball z q" "r + q \<le> s" shows "ball y r \<subseteq> ball z s" |
15 assumes "y \<in> ball z q" "r + q \<le> s" shows "ball y r \<subseteq> ball z s" |
16 proof safe |
16 using assms by metric |
17 fix x assume x: "x \<in> ball y r" |
|
18 have "dist z x \<le> dist z y + dist y x" |
|
19 by (rule dist_triangle) |
|
20 also have "\<dots> < s" |
|
21 using assms x by auto |
|
22 finally show "x \<in> ball z s" |
|
23 by simp |
|
24 qed |
|
25 |
17 |
26 lemma has_integral_implies_lebesgue_measurable_cbox: |
18 lemma has_integral_implies_lebesgue_measurable_cbox: |
27 fixes f :: "'a :: euclidean_space \<Rightarrow> real" |
19 fixes f :: "'a :: euclidean_space \<Rightarrow> real" |
28 assumes f: "(f has_integral I) (cbox x y)" |
20 assumes f: "(f has_integral I) (cbox x y)" |
29 shows "f \<in> lebesgue_on (cbox x y) \<rightarrow>\<^sub>M borel" |
21 shows "f \<in> lebesgue_on (cbox x y) \<rightarrow>\<^sub>M borel" |