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, becausea
andaᶜ
cannot simultaneously be in it.Set.Intersecting.is_max_iff_card_eq
: Any maximal intersecting family takes up half the elements.
References #
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)
:
@[simp]
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.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)
:
theorem
Set.Intersecting.exists_card_eq
{α : Type u_1}
[BooleanAlgebra α]
[Nontrivial α]
[Fintype α]
{s : Finset α}
(hs : (↑s).Intersecting)
: