# Zulip Chat Archive

## 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