Image and InjOn

Stream: Is there code for X?

[Patrick Massot]

Is there a proof of

lemma Set.exists_image_eq_and_injOn {α β : Type*} (f : α → β) (s : Set α) :
    ∃ u, f '' u =  f '' s ∧ InjOn f u

somewhere?
What about its immediate corollary

lemma Set.exists_image_of_subset_range {α β : Type*} {f : α → β} {s : Set β} (hs : s ⊆ range f) :
    ∃ t, f '' t = s ∧ InjOn f t

[Jireh Loreaux]

How about docs#Set.surjOn_iff_exists_bijOn_subset ?

[Patrick Massot]

I can prove those lemmas, but I'm very surprised I can't find them.

[Jireh Loreaux]

I mean, the lemma I linked is almost exactly the first thing you asked for with t instantiated as f '' s.

[Moritz Firsching]

docs#Function.invFunOn_injOn_image ?

[Patrick Massot]

Ok, so it seems we don't have those lemmas but indeed Jireh's proof is only

lemma Set.exists_image_eq_and_injOn {α β : Type*} (f : α → β) (s : Set α) :
    ∃ u, f '' u =  f '' s ∧ InjOn f u := by
  rcases surjOn_iff_exists_bijOn_subset.mp (surjOn_image f s) with ⟨u, hu, hfu⟩
  exact ⟨u, hfu.image_eq, hfu.injOn⟩

[Patrick Massot]

So that's an easy PR.

[Patrick Massot]

I'll PR it later today if nobody else does it in the mean-time (or find those lemmas already there).

[Patrick Massot]

Actually I had an unexpected time-slot and opened #8303.

[Jireh Loreaux]

I mentioned this on GitHub, but in case you prefer to discuss here: I think this is going in slightly the wrong way. I think we should be encouraging use of the Set.*On API, not inserting lemmas to avoid it.

[Jireh Loreaux]

If you strongly disagree, that's fine. I'm not going to push hard about this.

[Patrick Massot]

I don't understand this objection. The above proof is very short but it is still the combination of four lemmas, which is way above the bar to get a new lemma. And it is a very natural statement which clearly belongs to the very frustrating category of statements that are so intuitively obvious that even spending 1 minute thinking about how to convince Lean is very frustrating.

[Patrick Massot]

And InjOn appears in the conclusion so this is encouraging the use of the Set.*on API.

[Jireh Loreaux]

I guess my point is this: I don't expect you to ever want ∃ u, f '' u = f '' s ∧ InjOn f u by itself in context (but if I'm wrong, I'd be happy to see an example!). You will therefore always want to destructure it as ⟨u, hu, hfu⟩, but if you did that then you would have in context:

u : Set α
hu : f '' u = f '' s
hfu : InjOn f u

My claim is that this is less nice than destructuring the result of surjOn_iff_exists_bijOn_subset.mp (surjOn_image f s) directly as ⟨u, hu, hfu⟩, which results in the context

u : Set α
hu : u ⊆ s
hfu : BijOn f u (f '' s)

[Jireh Loreaux]

Then you get can to both f '' u = f '' s and InjOn f u with straightfoward applications of dot notation. But you also have easy access to API for SurjOn and BijOn, not to mention you know u ⊆ s, which might be handy (of course, this could be recovered in your version by modifying the lemma statement, but it isn't currently there). The BijOn bundle is much nicer than the unbundled alternative.

[Patrick Massot]

Again the actual target is

lemma exists_image_eq_injOn_of_subset_range {α β : Type*} {f : α → β} {t : Set β}
    (ht : t ⊆ range f) : ∃ s, f '' s = t ∧ InjOn f s

[Patrick Massot]

And the context was provided in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Compactness.20in.20Metric.20Spaces/near/401074057

[Patrick Massot]

The goal is to get a proof of compact.finite_subcover that is no more than 4 lines long.

[Jireh Loreaux]

4 lines if you add the following reasonable alias

import Mathlib

variable {X : Type} [MetricSpace X]
open Metric Set Function

def Open (S: Set X) := ∀x∈S, ∃r>0, (ball x r) ⊆ S
def Closed (S: Set X) := Open Sᶜ
def Bounded (S: Set X) := ∃r, ∃ x : X, S ⊆ ball x r
def Opencover (F: Set (Set X)) (S: Set X) := S ⊆ ⋃₀ F ∧ ∀f∈F, Open f
def finiteOpenCover (F: Set (Set X)) (S: Set X) := (Opencover F S) ∧ Set.Finite F
def compact (S : Set X) := ∀ F, Opencover F S → ∃ G, G ⊆ F ∧ finiteOpenCover G S

alias ⟨Set.SurjOn.exists_bijOn_subset, _⟩ := Set.surjOn_iff_exists_bijOn_subset

lemma compact.finite_subcover {S : Set X} (hS : compact S) {ι: Type*} {F : ι → Set X}
    (hF : ∀ i, Open (F i)) (hSF : S ⊆ ⋃ i, F i) :∃ I : Set ι, I.Finite ∧ S ⊆ ⋃ i ∈ I, F i := by
  obtain ⟨G, h₁, ⟨h₂, _⟩, h₃⟩ := hS (range F) ⟨sUnion_range F ▸ hSF, fun s ⟨i, h⟩ ↦ h ▸ hF i⟩
  obtain ⟨u, -, h⟩ := image_preimage_eq_of_subset h₁ ▸ surjOn_image .. |>.exists_bijOn_subset
  exact ⟨u, .of_finite_image (h.image_eq ▸ h₃) h.injOn, h₂.trans <| by
    rw [←h.image_eq, sUnion_image]⟩

[Jireh Loreaux]

@Patrick Massot whatever the outcome of the new lemmas, would you mind adding this alias to #8303? At the very least, that PR can clean up that declaration (as you have already done by fixing the existential binder).

alias ⟨Set.SurjOn.exists_bijOn_subset, _⟩ := Set.surjOn_iff_exists_bijOn_subset

[Patrick Massot]

I added the alias and merged so that we can discuss more interesting things.