compactness proof

Stream: new members

[Lambert A'Campo]

Could someone give me an example of a compactness proof in Lean?
For example assuming that the closed unit ball is compact,
there are finitely many points a_1, ..., a_n such that every any
point in the unit ball is at most 1/2 from one of the a_i.

[Kevin Buzzard]

import topology.metric_space.basic

example (X : Type*) [metric_space X] (O : X)
(Hcomp : compact {x : X | dist O x ≤ 1}) (r : ℝ) (hr : r > 0) :
  ∃ (A : finset X), ∀ x : X, ∃ a ∈ A, dist O x ≤ 1 → dist x a ≤ r :=
begin
  sorry
end

(any $r>0$ will do rather than $1/2$ I guess)

[Kevin Buzzard]

In discussions with Lambert I realised that compact_iff_finite_subcover is not an ideal first step in this proof.

[Kevin Buzzard]

Is something like compact (s : set X) iff forall J, forall f : J -> set X, (forall j, is_open f j) -> ... exists J' : finset J, ... in mathlib?

[Kevin Buzzard]

compact_iff_finite_subcover is compact s ↔ (∀c, (∀t∈c, is_open t) → s ⊆ ⋃₀ c → ∃c'⊆c, finite c' ∧ s ⊆ ⋃₀ c')

[Kevin Buzzard]

and here it would be easier to have the version involving an indexed family of opens