3399 h ` ({0..1} \<times> X) \<subseteq> Y \<and> |
3399 h ` ({0..1} \<times> X) \<subseteq> Y \<and> |
3400 (\<forall>x. h(0, x) = p x) \<and> |
3400 (\<forall>x. h(0, x) = p x) \<and> |
3401 (\<forall>x. h(1, x) = q x) \<and> |
3401 (\<forall>x. h(1, x) = q x) \<and> |
3402 (\<forall>t \<in> {0..1}. P(\<lambda>x. h(t, x))))" |
3402 (\<forall>t \<in> {0..1}. P(\<lambda>x. h(t, x))))" |
3403 |
3403 |
3404 |
|
3405 text\<open>$p, q$ are functions $X \to Y$, and the property $P$ restricts all intermediate maps. |
3404 text\<open>$p, q$ are functions $X \to Y$, and the property $P$ restricts all intermediate maps. |
3406 We often just want to require that $P$ fixes some subset, but to include the case of a loop homotopy, |
3405 We often just want to require that $P$ fixes some subset, but to include the case of a loop homotopy, |
3407 it is convenient to have a general property $P$.\<close> |
3406 it is convenient to have a general property $P$.\<close> |
3408 |
3407 |
3409 text \<open>We often want to just localize the ending function equality or whatever.\<close> |
3408 text \<open>We often want to just localize the ending function equality or whatever.\<close> |
|
3409 text%important \<open>%whitespace\<close> |
3410 proposition homotopic_with: |
3410 proposition homotopic_with: |
3411 fixes X :: "'a::topological_space set" and Y :: "'b::topological_space set" |
3411 fixes X :: "'a::topological_space set" and Y :: "'b::topological_space set" |
3412 assumes "\<And>h k. (\<And>x. x \<in> X \<Longrightarrow> h x = k x) \<Longrightarrow> (P h \<longleftrightarrow> P k)" |
3412 assumes "\<And>h k. (\<And>x. x \<in> X \<Longrightarrow> h x = k x) \<Longrightarrow> (P h \<longleftrightarrow> P k)" |
3413 shows "homotopic_with P X Y p q \<longleftrightarrow> |
3413 shows "homotopic_with P X Y p q \<longleftrightarrow> |
3414 (\<exists>h :: real \<times> 'a \<Rightarrow> 'b. |
3414 (\<exists>h :: real \<times> 'a \<Rightarrow> 'b. |