Intersecting families #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
theorem
set.intersecting.mono
{α : Type u_1}
[semilattice_inf α]
[order_bot α]
{s t : set α}
(h : t ⊆ s)
(hs : s.intersecting) :
theorem
set.intersecting.not_bot_mem
{α : Type u_1}
[semilattice_inf α]
[order_bot α]
{s : set α}
(hs : s.intersecting) :
theorem
set.intersecting.ne_bot
{α : Type u_1}
[semilattice_inf α]
[order_bot α]
{s : set α}
{a : α}
(hs : s.intersecting)
(ha : a ∈ s) :
@[simp]
theorem
set.intersecting_singleton
{α : Type u_1}
[semilattice_inf α]
[order_bot α]
{a : α} :
{a}.intersecting ↔ a ≠ ⊥
theorem
set.intersecting.insert
{α : Type u_1}
[semilattice_inf α]
[order_bot α]
{s : set α}
{a : α}
(hs : s.intersecting)
(ha : a ≠ ⊥)
(h : ∀ (b : α), b ∈ s → ¬disjoint a b) :
theorem
set.intersecting_insert
{α : Type u_1}
[semilattice_inf α]
[order_bot α]
{s : set α}
{a : α} :
(has_insert.insert a s).intersecting ↔ s.intersecting ∧ a ≠ ⊥ ∧ ∀ (b : α), b ∈ s → ¬disjoint a b
theorem
set.intersecting_iff_pairwise_not_disjoint
{α : Type u_1}
[semilattice_inf α]
[order_bot α]
{s : set α} :
@[protected]
theorem
set.subsingleton.intersecting
{α : Type u_1}
[semilattice_inf α]
[order_bot α]
{s : set α}
(hs : s.subsingleton) :
s.intersecting ↔ s ≠ {⊥}
theorem
set.intersecting_iff_eq_empty_of_subsingleton
{α : Type u_1}
[semilattice_inf α]
[order_bot α]
[subsingleton α]
(s : set α) :
s.intersecting ↔ s = ∅
@[protected]
theorem
set.intersecting.is_upper_set
{α : Type u_1}
[semilattice_inf α]
[order_bot α]
{s : set α}
(hs : s.intersecting)
(h : ∀ (t : set α), t.intersecting → s ⊆ t → s = t) :
Maximal intersecting families are upper sets.
theorem
set.intersecting.is_upper_set'
{α : Type u_1}
[semilattice_inf α]
[order_bot α]
{s : finset α}
(hs : ↑s.intersecting)
(h : ∀ (t : finset α), ↑t.intersecting → s ⊆ t → s = t) :
Maximal intersecting families are upper sets. Finset version.
theorem
set.intersecting.exists_mem_finset
{α : Type u_1}
[decidable_eq α]
{𝒜 : set (finset α)}
(h𝒜 : 𝒜.intersecting)
{s t : finset α}
(hs : s ∈ 𝒜)
(ht : t ∈ 𝒜) :
theorem
set.intersecting.not_compl_mem
{α : Type u_1}
[boolean_algebra α]
{s : set α}
(hs : s.intersecting)
{a : α}
(ha : a ∈ s) :
theorem
set.intersecting.not_mem
{α : Type u_1}
[boolean_algebra α]
{s : set α}
(hs : s.intersecting)
{a : α}
(ha : aᶜ ∈ s) :
a ∉ s
theorem
set.intersecting.disjoint_map_compl
{α : Type u_1}
[boolean_algebra α]
{s : finset α}
(hs : ↑s.intersecting) :
disjoint s (finset.map {to_fun := has_compl.compl (boolean_algebra.to_has_compl α), inj' := _} s)
theorem
set.intersecting.card_le
{α : Type u_1}
[boolean_algebra α]
[fintype α]
{s : finset α}
(hs : ↑s.intersecting) :
2 * s.card ≤ fintype.card α
theorem
set.intersecting.is_max_iff_card_eq
{α : Type u_1}
[boolean_algebra α]
[nontrivial α]
[fintype α]
{s : finset α}
(hs : ↑s.intersecting) :
theorem
set.intersecting.exists_card_eq
{α : Type u_1}
[boolean_algebra α]
[nontrivial α]
[fintype α]
{s : finset α}
(hs : ↑s.intersecting) :