disjoint sets in djsoint union

Stream: Is there code for X?

[Adam Topaz]

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]

Oh, maybe the correct answer is by tidy.

[Riccardo Brasca]

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

[Adam Topaz]

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

[Riccardo Brasca]

Sure! :+1:

[Eric Wieser]

Presumably docs#set.is_compl_range_inl_range_inr is a slightly stronger statement

[Eric Wieser]

Although I suppose .inf_eq_bot gives bot when you want empty

[Adam Topaz]

What about this simple thing?

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

[Adam Topaz]

Unfortunately, tidy doesn't solve this one :(

[Reid Barton]

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]

Thanks! Didn't know about set.image_inter

[Adam Topaz]

Should it be called image_inter_image?

[Kevin Buzzard]

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]

Oh now I have to go and find lean to check

[Kevin Buzzard]

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]

@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]

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

[Kevin Buzzard]

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]

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

[Eric Wieser]

Or have its equality reversed