equal
deleted
inserted
replaced
3641 |
3641 |
3642 lemma ivt_decreasing_component_on_1: fixes f::"real \<Rightarrow> 'a::euclidean_space" |
3642 lemma ivt_decreasing_component_on_1: fixes f::"real \<Rightarrow> 'a::euclidean_space" |
3643 assumes "a \<le> b" "continuous_on {a .. b} f" "(f b)$$k \<le> y" "y \<le> (f a)$$k" |
3643 assumes "a \<le> b" "continuous_on {a .. b} f" "(f b)$$k \<le> y" "y \<le> (f a)$$k" |
3644 shows "\<exists>x\<in>{a..b}. (f x)$$k = y" |
3644 shows "\<exists>x\<in>{a..b}. (f x)$$k = y" |
3645 apply(subst neg_equal_iff_equal[THEN sym]) |
3645 apply(subst neg_equal_iff_equal[THEN sym]) |
3646 using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"] using assms using continuous_on_neg |
3646 using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"] |
3647 by auto |
3647 using assms using continuous_on_minus by auto |
3648 |
3648 |
3649 lemma ivt_decreasing_component_1: fixes f::"real \<Rightarrow> 'a::euclidean_space" |
3649 lemma ivt_decreasing_component_1: fixes f::"real \<Rightarrow> 'a::euclidean_space" |
3650 shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f |
3650 shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f |
3651 \<Longrightarrow> f b$$k \<le> y \<Longrightarrow> y \<le> f a$$k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)$$k = y" |
3651 \<Longrightarrow> f b$$k \<le> y \<Longrightarrow> y \<le> f a$$k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)$$k = y" |
3652 by(rule ivt_decreasing_component_on_1) |
3652 by(rule ivt_decreasing_component_on_1) |