feat(Data/Rel): prove simple propositions about images, preimages and…

… graphs of relations (#6559)

Add lemmas about relation composition with top and bottom elements, conditions under which images under a relation form the whole codomain, and the equivalence between being a functional relation and representable by the graph of a function.



Co-authored-by: uniwuni <95649083+uniwuni@users.noreply.github.com>

Mathlib/Data/Rel.lean

@@ -5,6 +5,7 @@ Authors: Jeremy Avigad
 -/
 import Mathlib.Order.CompleteLattice
 import Mathlib.Order.GaloisConnection
+import Mathlib.Order.Hom.CompleteLattice
 
 #align_import data.rel from "leanprover-community/mathlib"@"706d88f2b8fdfeb0b22796433d7a6c1a010af9f2"
 
@@ -116,6 +117,26 @@ theorem comp_left_id (r : Rel α β) : @Eq α • r = r := by
   simp
 #align rel.comp_left_id Rel.comp_left_id
 
+@[simp]
+theorem comp_right_bot (r : Rel α β) : r • (⊥ : Rel β γ) = ⊥ := by
+  ext x y
+  simp [comp, Bot.bot]
+
+@[simp]
+theorem comp_left_bot (r : Rel α β) : (⊥ : Rel γ α) • r = ⊥ := by
+  ext x y
+  simp [comp, Bot.bot]
+
+@[simp]
+theorem comp_right_top (r : Rel α β) : r • (⊤ : Rel β γ) = λ x _ ↦ x ∈ r.dom := by
+  ext x z
+  simp [comp, Top.top, dom]
+
+@[simp]
+theorem comp_left_top (r : Rel α β) : (⊤ : Rel γ α) • r = λ _ y ↦ y ∈ r.codom := by
+  ext x z
+  simp [comp, Top.top, codom]
+
 theorem inv_id : inv (@Eq α) = @Eq α := by
   ext x y
   constructor <;> apply Eq.symm
@@ -126,6 +147,12 @@ theorem inv_comp (r : Rel α β) (s : Rel β γ) : inv (r • s) = inv s • inv
   simp [comp, inv, flip, and_comm]
 #align rel.inv_comp Rel.inv_comp
 
+@[simp]
+theorem inv_bot : (⊥ : Rel α β).inv = (⊥ : Rel β α) := by simp [Bot.bot, inv, flip]
+
+@[simp]
+theorem inv_top : (⊤ : Rel α β).inv = (⊤ : Rel β α) := by simp [Top.top, inv, flip]
+
 /-- Image of a set under a relation -/
 def image (s : Set α) : Set β := { y | ∃ x ∈ s, r x y }
 #align rel.image Rel.image
@@ -170,6 +197,22 @@ theorem image_univ : r.image Set.univ = r.codom := by
   simp [mem_image, codom]
 #align rel.image_univ Rel.image_univ
 
+@[simp]
+theorem image_empty : r.image ∅ = ∅ := by
+  ext x
+  simp [mem_image]
+
+@[simp]
+theorem image_bot (s : Set α) : (⊥ : Rel α β).image s = ∅ := by
+  rw [Set.eq_empty_iff_forall_not_mem]
+  intro x h
+  simp [mem_image, Bot.bot] at h
+
+@[simp]
+theorem image_top {s : Set α} (h : Set.Nonempty s) :
+    (⊤ : Rel α β).image s = Set.univ :=
+  Set.eq_univ_of_forall λ x ↦ ⟨h.some, by simp [h.some_mem, Top.top]⟩
+
 /-- Preimage of a set under a relation `r`. Same as the image of `s` under `r.inv` -/
 def preimage (s : Set β) : Set α :=
   r.inv.image s
@@ -206,6 +249,60 @@ theorem preimage_comp (s : Rel β γ) (t : Set γ) : preimage (r • s) t = prei
 theorem preimage_univ : r.preimage Set.univ = r.dom := by rw [preimage, image_univ, codom_inv]
 #align rel.preimage_univ Rel.preimage_univ
 
+@[simp]
+theorem preimage_empty : r.preimage ∅ = ∅ := by rw [preimage, image_empty]
+
+@[simp]
+theorem preimage_inv (s : Set α) : r.inv.preimage s = r.image s := by rw [preimage, inv_inv]
+
+@[simp]
+theorem preimage_bot (s : Set β) : (⊥ : Rel α β).preimage s = ∅ :=
+  by rw [preimage, inv_bot, image_bot]
+
+@[simp]
+theorem preimage_top {s : Set β} (h : Set.Nonempty s) :
+    (⊤ : Rel α β).preimage s = Set.univ := by rwa [← inv_top, preimage, inv_inv, image_top]
+
+theorem image_eq_dom_of_codomain_subset {s : Set β} (h : r.codom ⊆ s) : r.preimage s = r.dom := by
+  rw [← preimage_univ]
+  apply Set.eq_of_subset_of_subset
+  · exact image_subset _ (Set.subset_univ _)
+  · intro x hx
+    simp only [mem_preimage, Set.mem_univ, true_and] at hx
+    rcases hx with ⟨y, ryx⟩
+    have hy : y ∈ s := h ⟨x, ryx⟩
+    exact ⟨y, ⟨hy, ryx⟩⟩
+
+theorem preimage_eq_codom_of_domain_subset {s : Set α} (h : r.dom ⊆ s) : r.image s = r.codom :=
+  by apply r.inv.image_eq_dom_of_codomain_subset (by rwa [← codom_inv] at h)
+
+theorem image_inter_dom_eq (s : Set α) : r.image (s ∩ r.dom) = r.image s := by
+  apply Set.eq_of_subset_of_subset
+  · apply r.image_mono (by simp)
+  · intro x h
+    rw [mem_image] at *
+    rcases h with ⟨y, hy, ryx⟩
+    use y
+    suffices h : y ∈ r.dom by simp_all only [Set.mem_inter_iff, and_self]
+    rw [dom, Set.mem_setOf_eq]
+    use x
+
+@[simp]
+theorem preimage_inter_codom_eq (s : Set β) : r.preimage (s ∩ r.codom) = r.preimage s := by
+  rw[←dom_inv, preimage, preimage, image_inter_dom_eq]
+
+theorem inter_dom_subset_preimage_image (s : Set α) : s ∩ r.dom ⊆ r.preimage (r.image s) := by
+  intro x hx
+  simp only [Set.mem_inter_iff, dom] at hx
+  rcases hx with ⟨hx, ⟨y, rxy⟩⟩
+  use y
+  simp only [image, Set.mem_setOf_eq]
+  exact ⟨⟨x, hx, rxy⟩, rxy⟩
+
+theorem image_preimage_subset_inter_codom (s : Set β) : s ∩ r.codom ⊆ r.image (r.preimage s) := by
+  rw [← dom_inv, ← preimage_inv]
+  apply inter_dom_subset_preimage_image
+
 /-- Core of a set `s : Set β` w.r.t `r : Rel α β` is the set of `x : α` that are related *only*
 to elements of `s`. Other generalization of `Function.preimage`. -/
 def core (s : Set β) := { x | ∀ y, r x y → y ∈ s }
@@ -264,22 +361,52 @@ namespace Function
 def graph (f : α → β) : Rel α β := fun x y => f x = y
 #align function.graph Function.graph
 
+@[simp] lemma graph_def (f : α → β) (x y) : f.graph x y ↔ (f x = y) := Iff.rfl
+
+theorem graph_id : graph id = @Eq α := by simp [graph]
+
+theorem graph_comp {f : β → γ} {g : α → β} : graph (f ∘ g) = Rel.comp (graph g) (graph f) := by
+  ext x y
+  simp [Rel.comp]
+
 end Function
 
+theorem Equiv.graph_inv (f : α ≃ β) : (f.symm : β → α).graph = Rel.inv (f : α → β).graph := by
+  ext x y
+  aesop (add norm Rel.inv_def)
+
+theorem Relation.is_graph_iff (r : Rel α β) : (∃! f, Function.graph f = r) ↔ ∀ x, ∃! y, r x y := by
+  unfold Function.graph
+  constructor
+  · rintro ⟨f, rfl, _⟩ x
+    use f x
+    simp only [forall_eq', and_self]
+  · intro h
+    rcases Classical.axiomOfChoice (λ x ↦ (h x).exists) with ⟨f,hf⟩
+    use f
+    constructor
+    · ext x _
+      constructor
+      · rintro rfl
+        exact hf x
+      · exact (h x).unique (hf x)
+    · rintro _ rfl
+      exact funext hf
+
 namespace Set
 
 -- TODO: if image were defined with bounded quantification in corelib, the next two would
 -- be definitional
 theorem image_eq (f : α → β) (s : Set α) : f '' s = (Function.graph f).image s := by
-  simp [Set.image, Function.graph, Rel.image]
+  simp [Set.image, Rel.image]
 #align set.image_eq Set.image_eq
 
 theorem preimage_eq (f : α → β) (s : Set β) : f ⁻¹' s = (Function.graph f).preimage s := by
-  simp [Set.preimage, Function.graph, Rel.preimage, Rel.inv, flip, Rel.image]
+  simp [Set.preimage, Rel.preimage, Rel.inv, flip, Rel.image]
 #align set.preimage_eq Set.preimage_eq
 
 theorem preimage_eq_core (f : α → β) (s : Set β) : f ⁻¹' s = (Function.graph f).core s := by
-  simp [Set.preimage, Function.graph, Rel.core]
+  simp [Set.preimage, Rel.core]
 #align set.preimage_eq_core Set.preimage_eq_core
 
 end Set