Generalization of `set.image_inter_on`

Stream: Is there code for X?

[Rish Vaishnav]

Just wanted to make sure, does the following generalization of set.image_inter_on exist under some different form that I should be using?

theorem image_inter_on' {α β} {f : α → β} {s t : set α}
  (h : ∀x∈s, ∀y∈t, x ∉ s ∩ t → y ∉ s ∩ t → f x ≠ f y) :
  f '' s ∩ f '' t = f '' (s ∩ t) :=
subset.antisymm
  (assume b ⟨⟨a₁, ha₁, h₁⟩, ⟨a₂, ha₂, h₂⟩⟩,
    begin
      by_cases hs : a₁ ∈ s ∩ t ∨ a₂ ∈ s ∩ t,
      { cases hs;
        have := mem_image_of_mem f hs,
        rwa h₁.symm, rwa h₂.symm },
      have := not_or_distrib.mp hs,
      exact false.elim (h _ ha₁ _ ha₂ this.1 this.2 (by simp *)),
    end)
  (image_inter_subset _ _ _)

(though I wouldn't be surprised if we haven't found a use for this yet)

[Yury G. Kudryashov]

I think that we should replace docs#set.image_inter_on with this lemma:

theorem image_inter_on' {f : α → β} {s t : set α}
  (h : ∀ (x ∈ s \ t) (y ∈ t \ s), f x = f y → x = y) :
  f '' s ∩ f '' t = f '' (s ∩ t) :=
begin
  refine subset.antisymm _ (image_inter_subset _ _ _),
  rintro _ ⟨⟨a, has, hab⟩, ⟨b, hbt, rfl⟩⟩,
  by_cases hat : a ∈ t, { exact hab ▸ mem_image_of_mem f ⟨has, hat⟩ },
  by_cases hbs : b ∈ s, { exact mem_image_of_mem f ⟨hbs, hbt⟩ },
  obtain rfl := h a ⟨has, hat⟩ b ⟨hbt, hbs⟩ hab,
  exact (hbs has).elim
end

[Yury G. Kudryashov]

(or you can use a version of your proof)

[Yury G. Kudryashov]

IMHO ∀ (x ∈ s \ t) (y ∈ t \ s), is more readable than ∀x∈s, ∀y∈t, x ∉ s ∩ t → y ∉ s ∩ t

[Yury G. Kudryashov]

It makes no sense to leave both old and new version because currently set.image_inter_on is used exactly once.

[Rish Vaishnav]

Sounds good, thank you! (and I'll take a few hints from how you wrote your proof lol)

BTW the f x = f y → x = y in the hypothesis can be replaced with f x ≠ f y

[Rish Vaishnav]

theorem image_inter_on' {f : α → β} {s t : set α}
  (h : ∀ (x ∈ s \ t) (y ∈ t \ s), f x ≠ f y) :
  f '' s ∩ f '' t = f '' (s ∩ t) :=
begin
  refine subset.antisymm _ (image_inter_subset _ _ _),
  rintro _ ⟨⟨a, has, hab⟩, ⟨b, hbt, rfl⟩⟩,
  by_cases hat : a ∈ t, { exact hab ▸ mem_image_of_mem f ⟨has, hat⟩ },
  by_cases hbs : b ∈ s, { exact mem_image_of_mem f ⟨hbs, hbt⟩ },
  exact absurd hab (h a ⟨has, hat⟩ b ⟨hbt, hbs⟩)
end