## Stream: maths

### Topic: More compactness questions

#### Lambert A'Campo (Nov 12 2019 at 16:19):

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 (Nov 12 2019 at 16:35):

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

#### Reid Barton (Nov 12 2019 at 16:43):

Also the choose tactic.

#### Reid Barton (Nov 12 2019 at 16:50):

(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 (Nov 12 2019 at 16:51):

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

#### Sebastien Gouezel (Nov 12 2019 at 16:59):

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 (Nov 12 2019 at 17:08):

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.

Last updated: May 11 2021 at 16:22 UTC