feat(data/set/prod): set.off_diag (#16803)

Define the off-diagonal of a set, which is the set of pairs of points whose components are distinct.

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>



Co-authored-by: Kyle Miller <kmill31415@gmail.com>

src/data/set/prod.lean

@@ -16,6 +16,7 @@ type.
 * `set.prod`: Binary product of sets. For `s : set α`, `t : set β`, we have
   `s.prod t : set (α × β)`.
 * `set.diagonal`: Diagonal of a type. `set.diagonal α = {(x, x) | x : α}`.
+* `set.off_diag`: Off-diagonal. `s ×ˢ s` without the diagonal.
 * `set.pi`: Arbitrary product of sets.
 -/
 
@@ -332,6 +333,59 @@ lemma diag_preimage_prod_self (s : set α) : (λ x, (x, x)) ⁻¹' (s ×ˢ s) =
 
 end diagonal
 
+section off_diag
+variables {α : Type*} {s t : set α} {x : α × α} {a : α}
+
+/-- The off-diagonal of a set `s` is the set of pairs `(a, b)` with `a, b ∈ s` and `a ≠ b`. -/
+def off_diag (s : set α) : set (α × α) := {x | x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2}
+
+@[simp] lemma mem_off_diag : x ∈ s.off_diag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2 := iff.rfl
+
+lemma off_diag_mono : monotone (off_diag : set α → set (α × α)) :=
+λ s t h x, and.imp (@h _) $ and.imp_left $ @h _
+
+@[simp] lemma off_diag_nonempty : s.off_diag.nonempty ↔ s.nontrivial :=
+by simp [off_diag, set.nonempty, set.nontrivial]
+
+@[simp] lemma off_diag_eq_empty : s.off_diag = ∅ ↔ s.subsingleton :=
+by rw [←not_nonempty_iff_eq_empty, ←not_nontrivial_iff, off_diag_nonempty.not]
+
+alias off_diag_nonempty ↔ _ nontrivial.off_diag_nonempty
+alias off_diag_nonempty ↔ _ subsingleton.off_diag_eq_empty
+
+variables (s t)
+
+lemma off_diag_subset_prod : s.off_diag ⊆ s ×ˢ s := λ x hx, ⟨hx.1, hx.2.1⟩
+lemma off_diag_eq_sep_prod : s.off_diag = {x ∈ s ×ˢ s | x.1 ≠ x.2} := ext $ λ _, and.assoc.symm
+
+@[simp] lemma off_diag_empty : (∅ : set α).off_diag = ∅ := by simp
+@[simp] lemma off_diag_singleton (a : α) : ({a} : set α).off_diag = ∅ := by simp
+@[simp] lemma off_diag_univ : (univ : set α).off_diag = (diagonal α)ᶜ := ext $ by simp
+
+@[simp] lemma prod_sdiff_diagonal : s ×ˢ s \ diagonal α = s.off_diag := ext $ λ _, and.assoc
+@[simp] lemma disjoint_diagonal_off_diag : disjoint (diagonal α) s.off_diag := λ x hx, hx.2.2.2 hx.1
+
+lemma off_diag_inter : (s ∩ t).off_diag = s.off_diag ∩ t.off_diag :=
+ext $ λ x, by { simp only [mem_off_diag, mem_inter_iff], tauto }
+
+variables {s t}
+
+lemma off_diag_union (h : disjoint s t) :
+  (s ∪ t).off_diag = s.off_diag ∪ t.off_diag ∪ s ×ˢ t ∪ t ×ˢ s :=
+begin
+  rw [off_diag_eq_sep_prod, union_prod, prod_union, prod_union, union_comm _ (t ×ˢ t), union_assoc,
+    union_left_comm (s ×ˢ t), ←union_assoc, sep_union, sep_union, ←off_diag_eq_sep_prod,
+    ←off_diag_eq_sep_prod, sep_eq_self_iff_mem_true.2, ←union_assoc],
+  simp only [mem_union, mem_prod, ne.def, prod.forall],
+  rintro i j (⟨hi, hj⟩ | ⟨hi, hj⟩) rfl; exact h ⟨‹_›, ‹_›⟩,
+end
+
+lemma off_diag_insert (ha : a ∉ s) : (insert a s).off_diag = s.off_diag ∪ {a} ×ˢ s ∪ s ×ˢ {a} :=
+by { rw [insert_eq, union_comm, off_diag_union, off_diag_singleton, union_empty, union_right_comm],
+   rintro b ⟨hb, (rfl : b = a)⟩, exact ha hb }
+
+end off_diag
+
 /-! ### Cartesian set-indexed product of sets -/
 
 section pi