## Stream: Is there code for X?

### Topic: disjoint sets in djsoint union

#### 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


#### Adam Topaz (Nov 24 2020 at 21:04):

Oh, maybe the correct answer is by tidy.

#### Riccardo Brasca (Nov 24 2020 at 21:23):

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

#### Adam Topaz (Nov 24 2020 at 21:25):

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

Sure! :+1:

#### Eric Wieser (Nov 24 2020 at 21:43):

Presumably docs#set.is_compl_range_inl_range_inr is a slightly stronger statement

#### Eric Wieser (Nov 24 2020 at 21:44):

Although I suppose .inf_eq_bot gives bot when you want empty

#### Adam Topaz (Nov 24 2020 at 21:50):

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


#### Adam Topaz (Nov 24 2020 at 21:50):

Unfortunately, tidy doesn't solve this one :(

#### 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


#### Adam Topaz (Nov 24 2020 at 22:24):

Should it be called image_inter_image?

#### 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...

#### Kevin Buzzard (Nov 24 2020 at 22:31):

Oh now I have to go and find lean to check

#### 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

#### 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 := _


#### 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 :-)

#### 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)


#### Floris van Doorn (Nov 24 2020 at 22:39):

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

#### Eric Wieser (Nov 24 2020 at 22:59):

Or have its equality reversed

Last updated: May 16 2021 at 05:21 UTC