Zulip Chat Archive

Stream: Is there code for X?

Topic: disjoint sets in djsoint union


view this post on Zulip Adam Topaz (Nov 24 2020 at 21:03):

I'm sure this is in mathlib, but I can't find it...

example {α β : Type*} : set.range (sum.inl : α  α  β)  set.range (sum.inr : β  α  β) =  := sorry

view this post on Zulip Adam Topaz (Nov 24 2020 at 21:04):

Oh, maybe the correct answer is by tidy.

view this post on Zulip Riccardo Brasca (Nov 24 2020 at 21:23):

There is set.is_compl_range_inl_range_inr that is essentially what you want.

view this post on Zulip Adam Topaz (Nov 24 2020 at 21:25):

Yeah, but proving the example with this takes more characters than by tidy.

view this post on Zulip Riccardo Brasca (Nov 24 2020 at 21:27):

Sure! :+1:

view this post on Zulip Eric Wieser (Nov 24 2020 at 21:43):

Presumably docs#set.is_compl_range_inl_range_inr is a slightly stronger statement

view this post on Zulip Eric Wieser (Nov 24 2020 at 21:44):

Although I suppose .inf_eq_bot gives bot when you want empty

view this post on Zulip Adam Topaz (Nov 24 2020 at 21:50):

What about this simple thing?

example {α β : Type*} (f : α  β) (S T : set α) : function.injective f  S  T =   (f '' S)  (f '' T) =  :=  sorry

view this post on Zulip Adam Topaz (Nov 24 2020 at 21:50):

Unfortunately, tidy doesn't solve this one :(

view this post on Zulip Reid Barton (Nov 24 2020 at 22:09):

example {α β : Type*} (f : α  β) (S T : set α) : function.injective f  S  T =   (f '' S)  (f '' T) =  := begin
  intros hf hst,
  rw [set.image_inter hf, hst, set.image_empty],
end

view this post on Zulip Adam Topaz (Nov 24 2020 at 22:24):

Thanks! Didn't know about set.image_inter

view this post on Zulip Adam Topaz (Nov 24 2020 at 22:24):

Should it be called image_inter_image?

view this post on Zulip Kevin Buzzard (Nov 24 2020 at 22:30):

I'm guessing what the result is but maybe image_inter_distrib would also be a valid name. But I think the idea is that image_inter might be saying something about the image of an intersection, and there's precisely one obvious thing you can say about it. EDIT -- actually maybe there are two...

view this post on Zulip Kevin Buzzard (Nov 24 2020 at 22:31):

Oh now I have to go and find lean to check

view this post on Zulip Kevin Buzzard (Nov 24 2020 at 22:33):

I was claiming that image_inter could only mean one thing but it could also mean an inclusion for a non injective function

view this post on Zulip Adam Topaz (Nov 24 2020 at 22:35):

@Kevin Buzzard This is splitting hairs, but IMO image_inter would make more sense with the following type:

theorem image_inter {f : α  β} {s t : set α} (H : injective f) :
   f '' (s  t) = f '' s  f '' t := _

view this post on Zulip Kevin Buzzard (Nov 24 2020 at 22:36):

I agree! I realised I had to stop guessing what the function was and actually go and look :-)

view this post on Zulip Kevin Buzzard (Nov 24 2020 at 22:37):

For others who are also reading whilst washing up:

set.image_inter :
   {α : Type u_1} {β : Type u_2} {f : α  β} {s t : set α},
    function.injective f  f '' s  f '' t = f '' (s  t)

view this post on Zulip Floris van Doorn (Nov 24 2020 at 22:39):

Yes, maybe the lemma should be called image_inter_image after all.

view this post on Zulip Eric Wieser (Nov 24 2020 at 22:59):

Or have its equality reversed


Last updated: May 16 2021 at 05:21 UTC