Zulip Chat Archive

Stream: maths

Topic: More compactness questions


view this post on Zulip 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 ?

view this post on Zulip Chris Hughes (Nov 12 2019 at 16:35):

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

view this post on Zulip Reid Barton (Nov 12 2019 at 16:43):

Also the choose tactic.

view this post on Zulip 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.)

view this post on Zulip 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 ..."

view this post on Zulip 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.

view this post on Zulip 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