feat(Combinatorics/SetFamily/Intersecting): L-intersecting families (leanprover-community#34777)

Define L-intersecting families and establish their basic properties.

A family 𝒜 of finsets is L-intersecting if all pairwise intersection sizes of distinct members of 𝒜 belong to L ⊆ ℕ.

From LeanCamCombi.

Author: sqrt-of-2

Mathlib/Combinatorics/SetFamily/Intersecting.lean

@@ -20,6 +20,8 @@ This file defines intersecting families and proves their basic properties.
 * `Set.Intersecting.card_le`: An intersecting family can only take up to half the elements, because
   `a` and `aᶜ` cannot simultaneously be in it.
 * `Set.Intersecting.is_max_iff_card_eq`: Any maximal intersecting family takes up half the elements.
+* `Set.IsIntersectingOf`: Predicate stating that a family `𝒜` of finsets is `L`-intersecting, i.e.,
+  meaning the intersection size of every pair of distinct members of `𝒜` belongs to `L ⊆ ℕ`.
 
 ## References
 
@@ -32,12 +34,12 @@ assert_not_exists Monoid
 
 open Finset
 
-variable {α : Type*}
-
 namespace Set
 
 section SemilatticeInf
 
+variable {α : Type*}
+
 variable [SemilatticeInf α] [OrderBot α] {s t : Set α} {a b c : α}
 
 /-- A set family is intersecting if every pair of elements is non-disjoint. -/
@@ -122,6 +124,10 @@ theorem Intersecting.isUpperSet' {s : Finset α} (hs : (s : Set α).Intersecting
 
 end SemilatticeInf
 
+section
+
+variable {α : Type*}
+
 theorem Intersecting.exists_mem_set {𝒜 : Set (Set α)} (h𝒜 : 𝒜.Intersecting) {s t : Set α}
     (hs : s ∈ 𝒜) (ht : t ∈ 𝒜) : ∃ a, a ∈ s ∧ a ∈ t :=
   not_disjoint_iff.1 <| h𝒜 hs ht
@@ -189,4 +195,53 @@ theorem Intersecting.exists_card_eq (hs : (s : Set α).Intersecting) :
   rw [Nat.le_div_iff_mul_le Nat.two_pos, Nat.mul_comm]
   exact ht.card_le
 
+end
+
+/-!
+### `L`-intersecting families
+
+This section defines `L`-intersecting families and establishes their basic properties.
+-/
+
+variable {L L' : Set ℕ}
+variable {α : Type*} [DecidableEq α]
+variable {𝒜 ℬ : Set (Finset α)}
+
+/--
+A family `𝒜` of finite subsets of `α` is `L`-intersecting if the intersection size of every pair of
+distinct members of `𝒜` belongs to `L ⊆ ℕ`.
+
+That is, for all `s, t ∈ 𝒜` with `s ≠ t`, we have `|(s ∩ t)| ∈ L`.
+-/
+def IsIntersectingOf (L : Set ℕ) (𝒜 : Set (Finset α)) : Prop := 𝒜.Pairwise fun s t ↦ #(s ∩ t) ∈ L
+
+namespace IsIntersectingOf
+
+/--
+An `L`-intersecting family is also `L'`-intersecting whenever `L ⊆ L'`.
+-/
+@[gcongr]
+theorem mono (h : L ⊆ L') (hL : IsIntersectingOf L 𝒜) : IsIntersectingOf L' 𝒜 := by tauto
+
+/--
+An `L`-intersecting family remains `L`-intersecting under restriction to any subfamily.
+-/
+@[gcongr]
+theorem anti (h : ℬ ⊆ 𝒜) (h𝒜 : IsIntersectingOf L 𝒜) : IsIntersectingOf L ℬ := Pairwise.mono h h𝒜
+
+/--
+The empty family of finite sets is `L`-intersecting, vacuously, because it contains no pairs of
+sets.
+-/
+@[simp]
+protected theorem empty : IsIntersectingOf L (∅ : Set (Finset α)) := by tauto
+
+/--
+Every family of finite sets is `univ`-intersecting.
+-/
+@[simp]
+protected theorem univ : IsIntersectingOf univ 𝒜 := 𝒜.pairwise_of_forall _ fun _ _ ↦ trivial
+
+end IsIntersectingOf
+
 end Set