# 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} [] [] (s : Set α) :

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
Instances For
theorem Set.Intersecting.mono {α : Type u_1} [] [] {s : Set α} {t : Set α} (h : t s) (hs : s.Intersecting) :
t.Intersecting
theorem Set.Intersecting.not_bot_mem {α : Type u_1} [] [] {s : Set α} (hs : s.Intersecting) :
s
theorem Set.Intersecting.ne_bot {α : Type u_1} [] [] {s : Set α} {a : α} (hs : s.Intersecting) (ha : a s) :
theorem Set.intersecting_empty {α : Type u_1} [] [] :
.Intersecting
@[simp]
theorem Set.intersecting_singleton {α : Type u_1} [] [] {a : α} :
{a}.Intersecting a
theorem Set.Intersecting.insert {α : Type u_1} [] [] {s : Set α} {a : α} (hs : s.Intersecting) (ha : a ) (h : bs, ¬Disjoint a b) :
(insert a s).Intersecting
theorem Set.intersecting_insert {α : Type u_1} [] [] {s : Set α} {a : α} :
(insert a s).Intersecting s.Intersecting a bs, ¬Disjoint a b
theorem Set.intersecting_iff_pairwise_not_disjoint {α : Type u_1} [] [] {s : Set α} :
s.Intersecting (s.Pairwise fun (a b : α) => ¬Disjoint a b) s {}
theorem Set.Subsingleton.intersecting {α : Type u_1} [] [] {s : Set α} (hs : s.Subsingleton) :
s.Intersecting s {}
theorem Set.intersecting_iff_eq_empty_of_subsingleton {α : Type u_1} [] [] [] (s : Set α) :
s.Intersecting s =
theorem Set.Intersecting.isUpperSet {α : Type u_1} [] [] {s : Set α} (hs : s.Intersecting) (h : ∀ (t : Set α), t.Intersectings ts = t) :

Maximal intersecting families are upper sets.

theorem Set.Intersecting.isUpperSet' {α : Type u_1} [] [] {s : } (hs : (s).Intersecting) (h : ∀ (t : ), (t).Intersectings ts = t) :

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 𝒜) :
as, a t
theorem Set.Intersecting.exists_mem_finset {α : Type u_1} [] {𝒜 : Set ()} (h𝒜 : 𝒜.Intersecting) {s : } {t : } (hs : s 𝒜) (ht : t 𝒜) :
as, a t
theorem Set.Intersecting.not_compl_mem {α : Type u_1} [] {s : Set α} (hs : s.Intersecting) {a : α} (ha : a s) :
as
theorem Set.Intersecting.not_mem {α : Type u_1} [] {s : Set α} (hs : s.Intersecting) {a : α} (ha : a s) :
as
theorem Set.Intersecting.disjoint_map_compl {α : Type u_1} [] {s : } (hs : (s).Intersecting) :
Disjoint s (Finset.map { toFun := compl, inj' := } s)
theorem Set.Intersecting.card_le {α : Type u_1} [] [] {s : } (hs : (s).Intersecting) :
2 * s.card
theorem Set.Intersecting.is_max_iff_card_eq {α : Type u_1} [] [] [] {s : } (hs : (s).Intersecting) :
(∀ (t : ), (t).Intersectings ts = t) 2 * s.card =
theorem Set.Intersecting.exists_card_eq {α : Type u_1} [] [] [] {s : } (hs : (s).Intersecting) :
∃ (t : ), s t 2 * t.card = (t).Intersecting