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 #
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 t : Set α}
(h : t ⊆ s)
(hs : s.Intersecting)
:
theorem
Set.Intersecting.bot_notMem
{α : Type u_1}
[SemilatticeInf α]
[OrderBot α]
{s : Set α}
(hs : s.Intersecting)
:
⊥ ∉ s
@[deprecated Set.Intersecting.bot_notMem (since := "2025-05-24")]
theorem
Set.Intersecting.not_bot_mem
{α : Type u_1}
[SemilatticeInf α]
[OrderBot α]
{s : Set α}
(hs : s.Intersecting)
:
⊥ ∉ s
Alias of Set.Intersecting.bot_notMem.
theorem
Set.Intersecting.ne_bot
{α : Type u_1}
[SemilatticeInf α]
[OrderBot α]
{s : Set α}
{a : α}
(hs : s.Intersecting)
(ha : a ∈ s)
:
@[simp]
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 : α}
:
theorem
Set.Subsingleton.intersecting
{α : Type u_1}
[SemilatticeInf α]
[OrderBot α]
{s : Set α}
(hs : s.Subsingleton)
:
theorem
Set.intersecting_iff_eq_empty_of_subsingleton
{α : Type u_1}
[SemilatticeInf α]
[OrderBot α]
[Subsingleton α]
(s : Set α)
:
theorem
Set.Intersecting.isUpperSet
{α : Type u_1}
[SemilatticeInf α]
[OrderBot α]
{s : Set α}
(hs : s.Intersecting)
(h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t)
:
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
@[deprecated Set.Intersecting.compl_notMem (since := "2025-05-24")]
theorem
Set.Intersecting.not_compl_mem
{α : Type u_1}
[BooleanAlgebra α]
{s : Set α}
(hs : s.Intersecting)
{a : α}
(ha : a ∈ s)
:
aᶜ ∉ s
Alias of Set.Intersecting.compl_notMem.
theorem
Set.Intersecting.notMem
{α : Type u_1}
[BooleanAlgebra α]
{s : Set α}
(hs : s.Intersecting)
{a : α}
(ha : aᶜ ∈ s)
:
a ∉ s
@[deprecated Set.Intersecting.notMem (since := "2025-05-23")]
theorem
Set.Intersecting.not_mem
{α : Type u_1}
[BooleanAlgebra α]
{s : Set α}
(hs : s.Intersecting)
{a : α}
(ha : aᶜ ∈ s)
:
a ∉ s
Alias of Set.Intersecting.notMem.
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)
:
theorem
Set.Intersecting.is_max_iff_card_eq
{α : Type u_1}
[BooleanAlgebra α]
[Nontrivial α]
[Fintype α]
{s : Finset α}
(hs : (↑s).Intersecting)
:
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