equal
deleted
inserted
replaced
324 and nbnd: "\<And>f s. s \<in> simplices \<Longrightarrow> face f s \<Longrightarrow> \<not> bnd f \<Longrightarrow> card {s\<in>simplices. face f s} = 2" |
324 and nbnd: "\<And>f s. s \<in> simplices \<Longrightarrow> face f s \<Longrightarrow> \<not> bnd f \<Longrightarrow> card {s\<in>simplices. face f s} = 2" |
325 and odd_card: "odd (card {f. (\<exists>s\<in>simplices. face f s) \<and> rl ` f = {..n} \<and> bnd f})" |
325 and odd_card: "odd (card {f. (\<exists>s\<in>simplices. face f s) \<and> rl ` f = {..n} \<and> bnd f})" |
326 shows "odd (card {s\<in>simplices. (rl ` s = {..Suc n})})" |
326 shows "odd (card {s\<in>simplices. (rl ` s = {..Suc n})})" |
327 proof (rule kuhn_counting_lemma) |
327 proof (rule kuhn_counting_lemma) |
328 have finite_s[simp]: "\<And>s. s \<in> simplices \<Longrightarrow> finite s" |
328 have finite_s[simp]: "\<And>s. s \<in> simplices \<Longrightarrow> finite s" |
329 by (metis add_is_0 zero_neq_numeral card_infinite assms(3)) |
329 by (metis add_is_0 zero_neq_numeral card.infinite assms(3)) |
330 |
330 |
331 let ?F = "{f. \<exists>s\<in>simplices. face f s}" |
331 let ?F = "{f. \<exists>s\<in>simplices. face f s}" |
332 have F_eq: "?F = (\<Union>s\<in>simplices. \<Union>a\<in>s. {s - {a}})" |
332 have F_eq: "?F = (\<Union>s\<in>simplices. \<Union>a\<in>s. {s - {a}})" |
333 by (auto simp: face) |
333 by (auto simp: face) |
334 show "finite ?F" |
334 show "finite ?F" |