equal
deleted
inserted
replaced
13 where "lipschitz_on C U f \<longleftrightarrow> (0 \<le> C \<and> (\<forall>x \<in> U. \<forall>y\<in>U. dist (f x) (f y) \<le> C * dist x y))" |
13 where "lipschitz_on C U f \<longleftrightarrow> (0 \<le> C \<and> (\<forall>x \<in> U. \<forall>y\<in>U. dist (f x) (f y) \<le> C * dist x y))" |
14 |
14 |
15 open_bundle lipschitz_syntax |
15 open_bundle lipschitz_syntax |
16 begin |
16 begin |
17 notation\<^marker>\<open>tag important\<close> lipschitz_on (\<open>_-lipschitz'_on\<close> [1000]) |
17 notation\<^marker>\<open>tag important\<close> lipschitz_on (\<open>_-lipschitz'_on\<close> [1000]) |
18 end |
|
19 |
|
20 bundle no_lipschitz_syntax |
|
21 begin |
|
22 no_notation lipschitz_on (\<open>_-lipschitz'_on\<close> [1000]) |
|
23 end |
18 end |
24 |
19 |
25 lemma lipschitz_onI: "L-lipschitz_on X f" |
20 lemma lipschitz_onI: "L-lipschitz_on X f" |
26 if "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist (f x) (f y) \<le> L * dist x y" "0 \<le> L" |
21 if "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist (f x) (f y) \<le> L * dist x y" "0 \<le> L" |
27 using that by (auto simp: lipschitz_on_def) |
22 using that by (auto simp: lipschitz_on_def) |