# Zulip Chat Archive

## Stream: general

### Topic: Prove that the image of a map is finite

#### Klaus Mattis (Feb 01 2021 at 10:51):

Hello,

I'm relatively new to lean (I learned about lean a year ago, I did the natural numbers game, but only started to use it more seriously the last week).

So I thought a good starting project would be "a cont. bij. map from a compact space to a hausdorff space is a homeo".

At the moment I have a mostly working proof of "compact subset in a hausdorff space is closed", but I'm stuck at the following problem:

(To remind you, the proof is roughly the following: Let A be the compact set, let x be a point not in A, for every point in A choose a neighborhood disjoint to a neighborhood of x, get a finite subcover, and use the intersection of the corresponding neighborhoods of x as open nbhd of x disjoint to A)

So I have the finite subcover of A, and I built a "function" of the following type:

```
have f: Π u : subcover, { p : nhds_of X x | p.1 ∩ u = ∅ }, by ...
```

(for every open u in the subcover, we get a nbhd of x, which is disjoint to u)

Then our finite set of nbhds of x would be the range of this subcover, this works.

Now I have trouble showing that the range is finite.

I used `finite_image`

, but this does not work, because the function's domain is not the Type set X, but a subtype of it,

for it to work, one apparently needs a function `set X -> set X`

, and then it gives you that the image of `subcover`

is finite.

So I built the following "workaround":

I defined a function

` let tempfun : set X → set X := λ u, if hu : u ∈ subcover then (f ⟨u, by assumption⟩).1.1 else ∅,`

Then I proofed that the image of `subcover`

is finite by using `finite_image`

First question: Can we avoid this weird workarounds?

Second question: Later I need to use that `tempfun u = f (<u, hu>)`

, (where `hu : u ∈ subcover`

),

which should be a trivial proof, but I don't know how to do it.

Thanks in advance!

Apologies if these questions are dumb or obvious, but I searched the web for quite a while and found nothing helpful :(

#### Klaus Mattis (Feb 01 2021 at 10:55):

To be precise in the second question: I made a mistake, I want to show `tempfun u = f (<u, hu>).1.1`

. which gets the underlying set of the neighborhood with the condition that it is disjoint to u.

#### Eric Wieser (Feb 01 2021 at 10:59):

I think you'd be a lot more likely to get help with an #mwe, it's difficult to solve "how do I do this trivial proof" questions without having exactly the same set of lean-based hurdles in front of us as you do.

#### Kevin Buzzard (Feb 01 2021 at 11:03):

I proved compact subspace of a Hausdorff space is closed using this "classical" approach in one of my Twitch streams over the summer: the code is here. I wrote a lot of comments. In mathlib they give a completely different proof using filters.

#### Klaus Mattis (Feb 01 2021 at 11:16):

Ok, yeah looks like a great idea to make a mwe :)

So it would be the following code:

```
import topology.basic
open set
lemma image_of_fin_set_is_finite
(A : Type) (B : Type) (s : set A) (hs : finite s) (f : s → B)
: finite (range f) := begin
--exact finite_image f hs, does not work, since finite_image expects f to start at A
sorry,
end
```

And thanks, @Kevin Buzzard , I will look at your code!

#### Johan Commelin (Feb 01 2021 at 11:18):

@Klaus Mattis that code snippet is a bit "too minimal". Please include `import foobar.quux`

in the code snippets, so that people can copy paste them into a new file and immediately have compiling code.

#### Klaus Mattis (Feb 01 2021 at 11:22):

I edited it in the above code.

#### Johan Commelin (Feb 01 2021 at 11:29):

```
lemma image_of_fin_set_is_finite
(A : Type) (B : Type) (s : set A) (hs : finite s) (f : s → B) :
finite (range f) :=
begin
convert finite_range _,
exact hs.fintype
end
```

#### Klaus Mattis (Feb 01 2021 at 11:44):

Ok, thanks a lot!

Last updated: Dec 20 2023 at 11:08 UTC