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.

References

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

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 : Set α} {t : Set α} (h : t ⊆ s) (hs : s.Intersecting) : t.Intersecting

theorem Set.Intersecting.not_bot_mem {α : 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 : Set α} {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 : Finset α} {t : Finset α} (hs : s ∈ 𝒜) (ht : t ∈ 𝒜) : ∃ a ∈ s, a ∈ t

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

theorem Set.Intersecting.not_mem {α : 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