image_bUnion

Stream: new members

[Damiano Testa]

Dear All,

I am not completely sure what bUnion refers to exactly, but I found myself needing the lemma below.

Is it already in mathlib? I could not find it.
Is the name reasonable? I am under the impression that bUnion means that it is a union over elements in a type with a condition that these elements should belong to a subset of the Type, but I could be wrong!

lemma image_bUnion {α β : Type*} {f : α → β} {s : set α} :
  f '' ((⋃ i ∈ s, {i}) ) = (⋃ i ∈ s, f '' {i}) :=
begin
  refine ext (λ x, ⟨_, _⟩),
  { rintro ⟨a, ⟨_, ⟨b, rfl⟩, t, ⟨⟨bs, rfl⟩, ta⟩⟩, rfl⟩,
    refine mem_Union.mpr ⟨a, _⟩,
    rw [image_singleton, mem_Union, mem_singleton_iff.mp ta],
    exact ⟨bs, rfl⟩ },
  { rintro ⟨_, ⟨a, rfl⟩, _, ⟨d, rfl⟩, b, ⟨ba, rfl⟩⟩,
    rw [mem_singleton_iff.mp ba, mem_image, bUnion_of_singleton],
    exact ⟨a, d, rfl⟩ }
end

[Yakov Pechersky]

bUnion is "big Union", or the union of indexed sets. It would be over all the sets of a Type, if that type is fintype, or some set describing the indices. This is as far as I understand.

[Yakov Pechersky]

Your lemma is about the union of singletons of elements in s, right?

[Yakov Pechersky]

Isn't that just s?

[Damiano Testa]

Thanks for the explanation on the name! I thought that it was "bound Union", implying a restriction on the indexing variable!

I realize that the lemma above is not exactly what I need, either. So, I will try to make s work above and to produce the lemma that I actually want!

Thanks for the help!

[Yakov Pechersky]

Btw,

lemma image_bUnion {α β : Type*} {f : α → β} {s : set α} :
  f '' ((⋃ i ∈ s, {i}) ) = (⋃ i ∈ s, f '' {i}) :=
by ext; simp [eq_comm]

[Damiano Testa]

Your proof is much better! I had found my proof by cleaning up after tidy! For some reason, I do not like to use simp in my final versions, but in this case, the shortening is so significant, that it makes sense!

[Yakov Pechersky]

The advice I got from PR comments was that the more "API" or "foundational" lemmas are totally OK to have proofs like "ext; simp" because there isn't much insight into the proof bodies

[Yakov Pechersky]

That is, proofs that on paper or in person are like "oh that's obvious" can also have proof bodies that are like that. That way scrolling through a file, it's easy to notice that this isn't a significant result, but is truly a "lemma".

[Damiano Testa]

Ok, I had not realized this and it does seem like a good guiding principle! I am slowly getting the hang of what API means...

[Damiano Testa]

Back to figuring out exactly what lemma I need and then I will look for it in mathlib! Otherwise, I will extend this thread!

[Yakov Pechersky]

Note, I found the proof by first doing simp, and that didn't do much, so, how do we show equality of unions? By equality of the elements, so ext. Then ext, simp. That was almost right, but in the exists statement in the RHS of the iff, one of the equalities was flipped compared to the LHS. So I just included eq_comm in the simp set here.

[Damiano Testa]

Thanks for the details on how you found the proof! My strategy is also to start with simp, try tidy otherwise, finish the proof (if I can!), and finally clean up to leave no inbetween simp. I am still not too much onboard on giving hints to simp: I will try to remember about this!

[Damiano Testa]

After the discussion, it turns out that the lemma below actually does finish my proof. I thought that some lemma around Union_of_singleton could have worked, but I did not find it.

lemma setext {R : Type*} (s : set R) :
  s = ⋃ (i : s), {i} :=
by ext; simp

In case you want the more verbose proof, here it is:

lemma setext {R : Type*} (s : set R) :
  s = ⋃ (i : s), {i} :=
begin
  refine ext (λ x, ⟨λ xs, mem_Union.mpr ⟨⟨x, xs⟩, mem_singleton x⟩, _⟩),
  rintro ⟨-, ⟨⟨-, xs⟩, rfl⟩, ⟨⟩⟩,
  exact xs,
end

[Yakov Pechersky]

git grep of ⋃ i : gives very few results

[Yakov Pechersky]

So your firstlemma would be good simp lemma! You might call it this:

@[simp] lemma set.bUnion_of_singleton_of_coe {R : Type*} (s : set R) :
  (⋃ (i : s), {i} : set R) = s :=
by ext; simp

[Yakov Pechersky]

but this might now be no longer a bUnion but a Union instead.

[Yakov Pechersky]

as one can see by the simp lemmas used in the proof, they only mention Union, not bUnion.

[Patrick Massot]

Damiano, bUnion does stand for "bounded union". Did you read the relevant section of MIL?

[Eric Wieser]

@Yakov Pechersky, why the of_coe? What coercion is happening there?

[Yakov Pechersky]

Sorry for the mistake re "bounded Union" vs "big Union", correcting up top.

[Yakov Pechersky]

There is a coercion from set s to set R.

[Eric Wieser]

Is there a lemma to convert from a union over a subtype to a union over a condition?

[Eric Wieser]

I can't help feeling that Damiano posted a very similar problem before

[Kevin Buzzard]

(deleted)

[Damiano Testa]

Patrick, I probably had read that section, but at a time where it made much less sense than it might now. I will brush up on it again!

Eric, you are right that I struggle often with sets/subtype/coercions. I do not know if it is only me, or it is a common difficulty.

[Patrick Massot]

Eric Wieser said:

Is there a lemma to convert from a union over a subtype to a union over a condition?

Of course there is. Did you try library_search?

[Eric Wieser]

No, I was sending that from mobile without access to a shell

[Eric Wieser]

Damiano, my point was that I think a previous thread might have concluded "here is a lemma that ought to be in mathlib", but the lemma never made it.

[Damiano Testa]

Eric, you may be right, since I have been struggling with coercions and sets also for the strand with the discrete_topology stuff and with the Liouville PR. In any case, I have now created PR #5691, which adds this simp lemma. In maintaining the style of the previous result in the file, I changed the proof from

by ext; simp

to

ext $ by simp

[Damiano Testa]

I also discovered that the result bUnion_of_singleton (without _coe) exists in mathlib and is not a proof of this lemma. However, I am not entirely sure why the two statements are not equivalent.

[Damiano Testa]

In a similar spirit, I also created PR #5692, adding another bUnion lemma, this time for zero_loci!

I am trying to get as much as possible of what I have on is_open_map comap C into mathlib, before I will have to devote more time to teaching!

[Eric Wieser]

Here's the old thread: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/name-hunt.3A.20Union_of_singleton.3F

[Damiano Testa]

Eric: thank you very much for finding this! It was indeed the same issue: I had forgotten that I had asked about it already!

How did you find it? I feel that I am not so good at using the search feature on Zulip...

[Eric Wieser]

Patrick Massot said:

Eric Wieser said:

Is there a lemma to convert from a union over a subtype to a union over a condition?

Of course there is. Did you try library_search?

Library search found docs#set.bUnion_eq_Union, which solves:

lemma set.Union_subtype {α β : Type*} (s : set α) (f : α → set β) :
  (⋃ (i : s), f i) = ⋃ (i ∈ s), f i :=
  (set.bUnion_eq_Union s $ λ x _, f x).symm