equal
deleted
inserted
replaced
6 |
6 |
7 theory Erdoes_Szekeres |
7 theory Erdoes_Szekeres |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 subsection \<open>Addition to @{theory HOL.Lattices_Big} Theory\<close> |
11 subsection \<open>Addition to \<^theory>\<open>HOL.Lattices_Big\<close> Theory\<close> |
12 |
12 |
13 lemma Max_gr: |
13 lemma Max_gr: |
14 assumes "finite A" |
14 assumes "finite A" |
15 assumes "a \<in> A" "a > x" |
15 assumes "a \<in> A" "a > x" |
16 shows "x < Max A" |
16 shows "x < Max A" |
17 using assms Max_ge less_le_trans by blast |
17 using assms Max_ge less_le_trans by blast |
18 |
18 |
19 subsection \<open>Additions to @{theory HOL.Finite_Set} Theory\<close> |
19 subsection \<open>Additions to \<^theory>\<open>HOL.Finite_Set\<close> Theory\<close> |
20 |
20 |
21 lemma obtain_subset_with_card_n: |
21 lemma obtain_subset_with_card_n: |
22 assumes "n \<le> card S" |
22 assumes "n \<le> card S" |
23 obtains T where "T \<subseteq> S" "card T = n" |
23 obtains T where "T \<subseteq> S" "card T = n" |
24 proof - |
24 proof - |