More compactness questions

Stream: maths

[Lambert A'Campo]

Suppose I used compactness to show that

finite A ∧ X ⊆ ∪ a ∈ A, ball a 0.5

How can I construct a function A -> X which assigns to every x in X an a in A such that d(x,a) < 0.5 ?

[Chris Hughes]

Something like classical.some or classical.axiom_of_choice should be useful.

[Reid Barton]

Also the choose tactic.

[Reid Barton]

(You might not think you need choice because A is finite, but finite A is not a constructively useful form of finiteness so you need what Lean calls "choice" anyways. It's easier to just use choice, and not use the finite A hypothesis.)

[Reid Barton]

In particular you should first transform the other hypothesis into "for all x, there exists a in A, such that ..."

[Sebastien Gouezel]

The choose tactic is just designed for this. Here is a possible proof:

lemma foo [metric_space α] (A X : set α) (hX : X ⊆ (⋃a ∈ A, ball a 0.5))
  (a : α) (ha : a ∈ A) :
  ∃(f : α → α), ∀x, f x ∈ A ∧ (x ∈ X → x ∈ ball (f x) 0.5) :=
begin
  classical,
  have : ∀(x : α), ∃a, a ∈ A ∧ (x ∈ X → x ∈ ball a 0.5) :=
  begin
    assume x,
    by_cases h : x ∈ X,
    { simpa [h] using hX h },
    { exact ⟨a, ha, by simp [h]⟩ }
  end,
  choose f hf using this,
  exact ⟨f, λx, hf x⟩
end

Note that in the way I have formalised the statement, the fact that A is nonempty needs to be an assumption, as otherwise the statement is not true (if A and X are empty but the whole type is not). If you formalize it slightly differently (requesting only that f x belongs to A when x is in X, for instance), this will not be necessary any more. It could be a good exercise for you to try to prove this modified statement following the same lines.

[Reid Barton]

You should also be able to construct f : A -> X (meaning a function from the subtype defined by A to the subtype defined by X). That should avoid these classical, by_cases steps. On the other hand you have to pay careful attention to the difference between ∀ a ∈ A and ∀ a : A and you might need to do some packing and unpacking of subtypes.