Documentation

Mathlib.Combinatorics.SetFamily.Intersecting

Intersecting families #

This file defines intersecting families and proves their basic properties.

Main declarations #

References #

def Set.Intersecting {α : Type u_1} [SemilatticeInf α] [OrderBot α] (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} [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) :
    theorem Set.intersecting_empty {α : Type u_1} [SemilatticeInf α] [OrderBot α] :
    .Intersecting
    @[simp]
    theorem Set.intersecting_singleton {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a : α} :
    {a}.Intersecting a
    theorem Set.Intersecting.insert {α : Type u_1} [SemilatticeInf α] [OrderBot α] {s : Set α} {a : α} (hs : s.Intersecting) (ha : a ) (h : bs, ¬Disjoint a b) :
    (insert a s).Intersecting
    theorem Set.intersecting_insert {α : Type u_1} [SemilatticeInf α] [OrderBot α] {s : Set α} {a : α} :
    (insert a s).Intersecting s.Intersecting a bs, ¬Disjoint a b
    theorem Set.intersecting_iff_pairwise_not_disjoint {α : Type u_1} [SemilatticeInf α] [OrderBot α] {s : Set α} :
    s.Intersecting (s.Pairwise fun (a b : α) => ¬Disjoint a b) s {}
    theorem Set.Subsingleton.intersecting {α : Type u_1} [SemilatticeInf α] [OrderBot α] {s : Set α} (hs : s.Subsingleton) :
    s.Intersecting s {}
    theorem Set.intersecting_iff_eq_empty_of_subsingleton {α : Type u_1} [SemilatticeInf α] [OrderBot α] [Subsingleton α] (s : Set α) :
    s.Intersecting s =
    theorem Set.Intersecting.isUpperSet {α : Type u_1} [SemilatticeInf α] [OrderBot α] {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} [SemilatticeInf α] [OrderBot α] {s : Finset α} (hs : (s).Intersecting) (h : ∀ (t : Finset α), (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} [DecidableEq α] {𝒜 : Set (Finset α)} (h𝒜 : 𝒜.Intersecting) {s : Finset α} {t : Finset α} (hs : s 𝒜) (ht : t 𝒜) :
    as, a t
    theorem Set.Intersecting.not_compl_mem {α : Type u_1} [BooleanAlgebra α] {s : Set α} (hs : s.Intersecting) {a : α} (ha : a s) :
    as
    theorem Set.Intersecting.not_mem {α : Type u_1} [BooleanAlgebra α] {s : Set α} (hs : s.Intersecting) {a : α} (ha : a s) :
    as
    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) :
    (∀ (t : Finset α), (t).Intersectings ts = t) 2 * s.card = Fintype.card α
    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