equal
deleted
inserted
replaced
1476 lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f" |
1476 lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f" |
1477 unfolding continuous_on_def by (metis subset_eq tendsto_within_subset) |
1477 unfolding continuous_on_def by (metis subset_eq tendsto_within_subset) |
1478 |
1478 |
1479 lemma continuous_at_imp_continuous_on: "\<forall>x\<in>s. isCont f x \<Longrightarrow> continuous_on s f" |
1479 lemma continuous_at_imp_continuous_on: "\<forall>x\<in>s. isCont f x \<Longrightarrow> continuous_on s f" |
1480 by (auto intro: continuous_at_within simp: continuous_on_eq_continuous_within) |
1480 by (auto intro: continuous_at_within simp: continuous_on_eq_continuous_within) |
1481 |
|
1482 lemma isContI_continuous: "continuous (at x within UNIV) f \<Longrightarrow> isCont f x" |
|
1483 by simp |
|
1484 |
|
1485 lemma isCont_ident[continuous_intros, simp]: "isCont (\<lambda>x. x) a" |
|
1486 using continuous_ident by (rule isContI_continuous) |
|
1487 |
|
1488 lemmas isCont_const = continuous_const |
|
1489 |
1481 |
1490 lemma isCont_o2: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (\<lambda>x. g (f x)) a" |
1482 lemma isCont_o2: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (\<lambda>x. g (f x)) a" |
1491 unfolding isCont_def by (rule tendsto_compose) |
1483 unfolding isCont_def by (rule tendsto_compose) |
1492 |
1484 |
1493 lemma isCont_o[continuous_intros]: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (g \<circ> f) a" |
1485 lemma isCont_o[continuous_intros]: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (g \<circ> f) a" |