equal
deleted
inserted
replaced
1410 ultimately show ?thesis |
1410 ultimately show ?thesis |
1411 by (rule_tac x="e/2" in exI) auto |
1411 by (rule_tac x="e/2" in exI) auto |
1412 qed |
1412 qed |
1413 |
1413 |
1414 |
1414 |
1415 section \<open>Path component, considered as a "joinability" relation (from Tom Hales)\<close> |
1415 section \<open>Path component, considered as a "joinability" relation\<close> |
|
1416 |
|
1417 text \<open>(by Tom Hales)\<close> |
1416 |
1418 |
1417 definition%important "path_component s x y \<longleftrightarrow> |
1419 definition%important "path_component s x y \<longleftrightarrow> |
1418 (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)" |
1420 (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)" |
1419 |
1421 |
1420 abbreviation%important |
1422 abbreviation%important |