Intersecting families

This file defines intersecting families and proves their basic properties.

Main declarations

• Set.Intersecting: Predicate for a set of elements in a generalized Boolean algebra to be an intersecting family.
• 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

• D. J. Kleitman, Families of non-disjoint subsets

def Set.Intersecting {α : Type u_1} [SemilatticeInf α] [OrderBot α] (s : Set α) : Prop

A set family is intersecting if every pair of elements is non-disjoint.

Equations

• s.Intersecting = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → ¬Disjoint a b

theorem Set.Intersecting.mono {α : Type u_1} [SemilatticeInf α] [OrderBot α] {s t : Set α} (h : t ⊆ s) (hs : s.Intersecting) : t.Intersecting

theorem Set.Intersecting.bot_notMem {α : Type u_1} [SemilatticeInf α] [OrderBot α] {s : Set α} (hs : s.Intersecting) : ⊥ ∉ s

theorem Set.Intersecting.ne_bot {α : Type u_1} [SemilatticeInf α] [OrderBot α] {s : Set α} {a : α} (hs : s.Intersecting) (ha : a ∈ s) : a ≠ ⊥

theorem Set.intersecting_empty {α : Type u_1} [SemilatticeInf α] [OrderBot α] : ∅.Intersecting

@[simp]

theorem Set.intersecting_singleton {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a : α} : {a}.Intersecting ↔ a ≠ ⊥

theorem Set.Intersecting.insert {α : Type u_1} [SemilatticeInf α] [OrderBot α] {s : Set α} {a : α} (hs : s.Intersecting) (ha : a ≠ ⊥) (h : ∀ b ∈ s, ¬Disjoint a b) : (insert a s).Intersecting

theorem Set.intersecting_insert {α : Type u_1} [SemilatticeInf α] [OrderBot α] {s : Set α} {a : α} : (insert a s).Intersecting ↔ s.Intersecting ∧ a ≠ ⊥ ∧ ∀ b ∈ s, ¬Disjoint a b

theorem Set.intersecting_iff_pairwise_not_disjoint {α : Type u_1} [SemilatticeInf α] [OrderBot α] {s : Set α} : s.Intersecting ↔ (s.Pairwise fun (a b : α) => ¬Disjoint a b) ∧ s ≠ {⊥}

theorem Set.Subsingleton.intersecting {α : Type u_1} [SemilatticeInf α] [OrderBot α] {s : Set α} (hs : s.Subsingleton) : s.Intersecting ↔ s ≠ {⊥}

theorem Set.intersecting_iff_eq_empty_of_subsingleton {α : Type u_1} [SemilatticeInf α] [OrderBot α] [Subsingleton α] (s : Set α) : s.Intersecting ↔ s = ∅

theorem Set.Intersecting.isUpperSet {α : Type u_1} [SemilatticeInf α] [OrderBot α] {s : Set α} (hs : s.Intersecting) (h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t) : IsUpperSet s

Maximal intersecting families are upper sets.

theorem Set.Intersecting.isUpperSet' {α : Type u_1} [SemilatticeInf α] [OrderBot α] {s : Finset α} (hs : (↑s).Intersecting) (h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t) : IsUpperSet ↑s

Maximal intersecting families are upper sets. Finset version.

theorem Set.Intersecting.exists_mem_set {α : Type u_1} {𝒜 : Set (Set α)} (h𝒜 : 𝒜.Intersecting) {s t : Set α} (hs : s ∈ 𝒜) (ht : t ∈ 𝒜) : ∃ a ∈ s, a ∈ t

theorem Set.Intersecting.exists_mem_finset {α : Type u_1} [DecidableEq α] {𝒜 : Set (Finset α)} (h𝒜 : 𝒜.Intersecting) {s t : Finset α} (hs : s ∈ 𝒜) (ht : t ∈ 𝒜) : ∃ a ∈ s, a ∈ t

theorem Set.Intersecting.compl_notMem {α : Type u_1} [BooleanAlgebra α] {s : Set α} (hs : s.Intersecting) {a : α} (ha : a ∈ s) : aᶜ ∉ s

theorem Set.Intersecting.notMem {α : Type u_1} [BooleanAlgebra α] {s : Set α} (hs : s.Intersecting) {a : α} (ha : aᶜ ∈ s) : a ∉ s

theorem Set.Intersecting.disjoint_map_compl {α : Type u_1} [BooleanAlgebra α] {s : Finset α} (hs : (↑s).Intersecting) : Disjoint s (Finset.map { toFun := compl, inj' := ⋯ } s)

theorem Set.Intersecting.card_le {α : Type u_1} [BooleanAlgebra α] [Fintype α] {s : Finset α} (hs : (↑s).Intersecting) : 2 * s.card ≤ Fintype.card α

theorem Set.Intersecting.is_max_iff_card_eq {α : Type u_1} [BooleanAlgebra α] [Nontrivial α] [Fintype α] {s : Finset α} (hs : (↑s).Intersecting) : (∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t) ↔ 2 * s.card = Fintype.card α

theorem Set.Intersecting.exists_card_eq {α : Type u_1} [BooleanAlgebra α] [Nontrivial α] [Fintype α] {s : Finset α} (hs : (↑s).Intersecting) : ∃ (t : Finset α), s ⊆ t ∧ 2 * t.card = Fintype.card α ∧ (↑t).Intersecting

L-intersecting families

This section defines L-intersecting families and establishes their basic properties.

def Set.IsIntersectingOf {α : Type u_1} [DecidableEq α] (L : Set ℕ) (𝒜 : Set (Finset α)) : Prop

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.

Equations

• L.IsIntersectingOf 𝒜 = 𝒜.Pairwise fun (s t : Finset α) => (s ∩ t).card ∈ L

theorem Set.IsIntersectingOf.mono {L L' : Set ℕ} {α : Type u_1} [DecidableEq α] {𝒜 : Set (Finset α)} (h : L ⊆ L') (hL : L.IsIntersectingOf 𝒜) : L'.IsIntersectingOf 𝒜

An L-intersecting family is also L'-intersecting whenever L ⊆ L'.

theorem Set.IsIntersectingOf.anti {L : Set ℕ} {α : Type u_1} [DecidableEq α] {𝒜 ℬ : Set (Finset α)} (h : ℬ ⊆ 𝒜) (h𝒜 : L.IsIntersectingOf 𝒜) : L.IsIntersectingOf ℬ

An L-intersecting family remains L-intersecting under restriction to any subfamily.

@[simp]

theorem Set.IsIntersectingOf.empty {L : Set ℕ} {α : Type u_1} [DecidableEq α] : L.IsIntersectingOf ∅

The empty family of finite sets is L-intersecting, vacuously, because it contains no pairs of sets.

@[simp]

theorem Set.IsIntersectingOf.univ {α : Type u_1} [DecidableEq α] {𝒜 : Set (Finset α)} : univ.IsIntersectingOf 𝒜

Every family of finite sets is univ-intersecting.