feat(data/set/lattice): Preimages are disjoint iff the sets are disjo…

…int (#14951)

Prove `disjoint (f ⁻¹' s) (f ⁻¹' t) ↔ disjoint s t` and `disjoint (f '' s) (f '' t) ↔ disjoint s t` when `f` is surjective/injective. Delete `set.disjoint_preimage` in favor of `disjoint.preimage`. Fix the statement of `set.preimage_eq_empty_iff` (the name referred to the RHS).

src/data/set/lattice.lean

@@ -1465,7 +1465,7 @@ We define some lemmas in the `disjoint` namespace to be able to use projection n
 
 section disjoint
 
-variables {s t u : set α}
+variables {s t u : set α} {f : α → β}
 
 namespace disjoint
 
@@ -1584,23 +1584,36 @@ lemma disjoint_image_of_injective {f : α → β} (hf : injective f) {s t : set
   (hd : disjoint s t) : disjoint (f '' s) (f '' t) :=
 disjoint_image_image $ λ x hx y hy, hf.ne $ λ H, set.disjoint_iff.1 hd ⟨hx, H.symm ▸ hy⟩
 
-lemma disjoint_preimage {s t : set β} (hd : disjoint s t) (f : α → β) :
-  disjoint (f ⁻¹' s) (f ⁻¹' t) :=
-λ x hx, hd hx
+lemma _root_.disjoint.inter_eq : disjoint s t → s ∩ t = ∅ := disjoint.eq_bot
+
+lemma _root_.disjoint.of_image (h : disjoint (f '' s) (f '' t)) : disjoint s t :=
+λ x hx, disjoint_left.1 h (mem_image_of_mem _ hx.1) (mem_image_of_mem _ hx.2)
+
+lemma disjoint_image_iff (hf : injective f) : disjoint (f '' s) (f '' t) ↔ disjoint s t :=
+⟨disjoint.of_image, disjoint_image_of_injective hf⟩
+
+lemma _root_.disjoint.of_preimage (hf : surjective f) {s t : set β}
+  (h : disjoint (f ⁻¹' s) (f ⁻¹' t)) :
+  disjoint s t :=
+by rw [disjoint_iff_inter_eq_empty, ←image_preimage_eq (_ ∩ _) hf, preimage_inter, h.inter_eq,
+  image_empty]
+
+lemma disjoint_preimage_iff (hf : surjective f) {s t : set β} :
+  disjoint (f ⁻¹' s) (f ⁻¹' t) ↔ disjoint s t :=
+⟨disjoint.of_preimage hf, disjoint.preimage _⟩
 
 lemma preimage_eq_empty {f : α → β} {s : set β} (h : disjoint s (range f)) :
   f ⁻¹' s = ∅ :=
 by simpa using h.preimage f
 
-lemma preimage_eq_empty_iff {f : α → β} {s : set β} : disjoint s (range f) ↔ f ⁻¹' s = ∅ :=
-⟨preimage_eq_empty,
-  λ h, begin
+lemma preimage_eq_empty_iff {s : set β} : f ⁻¹' s = ∅ ↔ disjoint s (range f) :=
+⟨λ h, begin
     simp only [eq_empty_iff_forall_not_mem, disjoint_iff_inter_eq_empty, not_exists,
       mem_inter_eq, not_and, mem_range, mem_preimage] at h ⊢,
     assume y hy x hx,
     rw ← hx at hy,
     exact h x hy,
-  end ⟩
+  end, preimage_eq_empty⟩
 
 lemma disjoint_iff_subset_compl_right :
   disjoint s t ↔ s ⊆ tᶜ :=

src/topology/tietze_extension.lean

@@ -61,7 +61,7 @@ begin
   have hc₂ : is_closed (e '' (f ⁻¹' (Ici (∥f∥ / 3)))),
     from he.is_closed_map _ (is_closed_Ici.preimage f.continuous),
   have hd : disjoint (e '' (f ⁻¹' (Iic (-∥f∥ / 3)))) (e '' (f ⁻¹' (Ici (∥f∥ / 3)))),
-  { refine disjoint_image_of_injective he.inj (disjoint_preimage _ _),
+  { refine disjoint_image_of_injective he.inj (disjoint.preimage _ _),
     rwa [Iic_disjoint_Ici, not_le] },
   rcases exists_bounded_mem_Icc_of_closed_of_le hc₁ hc₂ hd hf3.le with ⟨g, hg₁, hg₂, hgf⟩,
   refine ⟨g, _, _⟩,
@@ -219,7 +219,7 @@ begin
     function `dg : Y → ℝ` such that `dg ∘ e = 0`, `dg y = 0` whenever `c ≤ g y`, `dg y = c - a`
     whenever `g y = a`, and `0 ≤ dg y ≤ c - a` for all `y`.  -/
     have hd : disjoint (range e ∪ g ⁻¹' (Ici c)) (g ⁻¹' {a}),
-    { refine disjoint_union_left.2 ⟨_, disjoint_preimage _ _⟩,
+    { refine disjoint_union_left.2 ⟨_, disjoint.preimage _ _⟩,
       { rintro _ ⟨⟨x, rfl⟩, rfl : g (e x) = a⟩,
         exact ha' ⟨x, (congr_fun hgf x).symm⟩ },
       { exact set.disjoint_singleton_right.2 hac.not_le } },
@@ -248,7 +248,7 @@ begin
   rcases em (∃ x, f x = b) with ⟨x, rfl⟩|hb',
   { exact ⟨g, λ y, ⟨xl y, x, hxl y, hgb y⟩, hgf⟩ },
   have hd : disjoint (range e ∪ g ⁻¹' (Iic c)) (g ⁻¹' {b}),
-  { refine disjoint_union_left.2 ⟨_, disjoint_preimage _ _⟩,
+  { refine disjoint_union_left.2 ⟨_, disjoint.preimage _ _⟩,
     { rintro _ ⟨⟨x, rfl⟩, rfl : g (e x) = b⟩,
       exact hb' ⟨x, (congr_fun hgf x).symm⟩ },
     { exact set.disjoint_singleton_right.2 hcb.not_le } },