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, becauseaandaᶜ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]
A set family is intersecting if every pair of elements is non-disjoint.
Instances For
theorem
Set.Intersecting.mono
{α : Type u_1}
[SemilatticeInf α]
[OrderBot α]
{s : Set α}
{t : Set α}
(h : t ⊆ s)
(hs : Set.Intersecting s)
:
theorem
Set.Intersecting.not_bot_mem
{α : Type u_1}
[SemilatticeInf α]
[OrderBot α]
{s : Set α}
(hs : Set.Intersecting s)
:
⊥ ∉ s
theorem
Set.Intersecting.ne_bot
{α : Type u_1}
[SemilatticeInf α]
[OrderBot α]
{s : Set α}
{a : α}
(hs : Set.Intersecting s)
(ha : a ∈ s)
:
@[simp]
theorem
Set.intersecting_singleton
{α : Type u_1}
[SemilatticeInf α]
[OrderBot α]
{a : α}
:
Set.Intersecting {a} ↔ a ≠ ⊥
theorem
Set.Intersecting.insert
{α : Type u_1}
[SemilatticeInf α]
[OrderBot α]
{s : Set α}
{a : α}
(hs : Set.Intersecting s)
(ha : a ≠ ⊥)
(h : ∀ b ∈ s, ¬Disjoint a b)
:
Set.Intersecting (insert a s)
theorem
Set.intersecting_insert
{α : Type u_1}
[SemilatticeInf α]
[OrderBot α]
{s : Set α}
{a : α}
:
Set.Intersecting (insert a s) ↔ Set.Intersecting s ∧ a ≠ ⊥ ∧ ∀ b ∈ s, ¬Disjoint a b
theorem
Set.intersecting_iff_pairwise_not_disjoint
{α : Type u_1}
[SemilatticeInf α]
[OrderBot α]
{s : Set α}
:
Set.Intersecting s ↔ (Set.Pairwise s fun (a b : α) => ¬Disjoint a b) ∧ s ≠ {⊥}
theorem
Set.Subsingleton.intersecting
{α : Type u_1}
[SemilatticeInf α]
[OrderBot α]
{s : Set α}
(hs : Set.Subsingleton s)
:
Set.Intersecting s ↔ s ≠ {⊥}
theorem
Set.intersecting_iff_eq_empty_of_subsingleton
{α : Type u_1}
[SemilatticeInf α]
[OrderBot α]
[Subsingleton α]
(s : Set α)
:
Set.Intersecting s ↔ s = ∅
theorem
Set.Intersecting.isUpperSet
{α : Type u_1}
[SemilatticeInf α]
[OrderBot α]
{s : Set α}
(hs : Set.Intersecting s)
(h : ∀ (t : Set α), Set.Intersecting t → s ⊆ t → s = t)
:
Maximal intersecting families are upper sets.
theorem
Set.Intersecting.isUpperSet'
{α : Type u_1}
[SemilatticeInf α]
[OrderBot α]
{s : Finset α}
(hs : Set.Intersecting ↑s)
(h : ∀ (t : Finset α), Set.Intersecting ↑t → s ⊆ t → s = t)
:
IsUpperSet ↑s
Maximal intersecting families are upper sets. Finset version.
theorem
Set.Intersecting.exists_mem_finset
{α : Type u_1}
[DecidableEq α]
{𝒜 : Set (Finset α)}
(h𝒜 : Set.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 : Set.Intersecting s)
{a : α}
(ha : a ∈ s)
:
aᶜ ∉ s
theorem
Set.Intersecting.not_mem
{α : Type u_1}
[BooleanAlgebra α]
{s : Set α}
(hs : Set.Intersecting s)
{a : α}
(ha : aᶜ ∈ s)
:
a ∉ s
theorem
Set.Intersecting.disjoint_map_compl
{α : Type u_1}
[BooleanAlgebra α]
{s : Finset α}
(hs : Set.Intersecting ↑s)
:
Disjoint s (Finset.map { toFun := compl, inj' := ⋯ } s)
theorem
Set.Intersecting.card_le
{α : Type u_1}
[BooleanAlgebra α]
[Fintype α]
{s : Finset α}
(hs : Set.Intersecting ↑s)
:
2 * s.card ≤ Fintype.card α
theorem
Set.Intersecting.is_max_iff_card_eq
{α : Type u_1}
[BooleanAlgebra α]
[Nontrivial α]
[Fintype α]
{s : Finset α}
(hs : Set.Intersecting ↑s)
:
(∀ (t : Finset α), Set.Intersecting ↑t → s ⊆ t → s = t) ↔ 2 * s.card = Fintype.card α
theorem
Set.Intersecting.exists_card_eq
{α : Type u_1}
[BooleanAlgebra α]
[Nontrivial α]
[Fintype α]
{s : Finset α}
(hs : Set.Intersecting ↑s)
:
∃ (t : Finset α), s ⊆ t ∧ 2 * t.card = Fintype.card α ∧ Set.Intersecting ↑t