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.

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.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 : α} :
    theorem Set.Intersecting.insert {α : Type u_1} [SemilatticeInf α] [OrderBot α] {s : Set α} {a : α} (hs : Set.Intersecting s) (ha : a ) (h : ∀ (b : α), b s¬Disjoint a b) :
    theorem Set.intersecting_insert {α : Type u_1} [SemilatticeInf α] [OrderBot α] {s : Set α} {a : α} :
    Set.Intersecting (insert a s) Set.Intersecting s a ∀ (b : α), b s¬Disjoint a b
    theorem Set.Intersecting.isUpperSet {α : Type u_1} [SemilatticeInf α] [OrderBot α] {s : Set α} (hs : Set.Intersecting s) (h : ∀ (t : Set α), Set.Intersecting ts ts = 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 ts ts = t) :

    Maximal intersecting families are upper sets. Finset version.

    theorem Set.Intersecting.exists_mem_set {α : Type u_1} {𝒜 : Set (Set α)} (h𝒜 : Set.Intersecting 𝒜) {s : Set α} {t : Set α} (hs : s 𝒜) (ht : t 𝒜) :
    a, a s a t
    theorem Set.Intersecting.exists_mem_finset {α : Type u_1} [DecidableEq α] {𝒜 : Set (Finset α)} (h𝒜 : Set.Intersecting 𝒜) {s : Finset α} {t : Finset α} (hs : s 𝒜) (ht : t 𝒜) :
    a, a s a t
    theorem Set.Intersecting.not_compl_mem {α : Type u_1} [BooleanAlgebra α] {s : Set α} (hs : Set.Intersecting s) {a : α} (ha : 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' := (_ : Function.Injective compl) } s)
    theorem Set.Intersecting.is_max_iff_card_eq {α : Type u_1} [BooleanAlgebra α] [Nontrivial α] [Fintype α] {s : Finset α} (hs : Set.Intersecting s) :
    (∀ (t : Finset α), Set.Intersecting ts ts = t) 2 * Finset.card s = Fintype.card α