equal
deleted
inserted
replaced
6 section \<open>Helly's selection theorem\<close> |
6 section \<open>Helly's selection theorem\<close> |
7 |
7 |
8 text \<open>The set of bounded, monotone, right continuous functions is sequentially compact\<close> |
8 text \<open>The set of bounded, monotone, right continuous functions is sequentially compact\<close> |
9 |
9 |
10 theory Helly_Selection |
10 theory Helly_Selection |
11 imports "~~/src/HOL/Library/Diagonal_Subsequence" Weak_Convergence |
11 imports "HOL-Library.Diagonal_Subsequence" Weak_Convergence |
12 begin |
12 begin |
13 |
13 |
14 lemma minus_one_less: "x - 1 < (x::real)" |
14 lemma minus_one_less: "x - 1 < (x::real)" |
15 by simp |
15 by simp |
16 |
16 |