# mathlib3documentation

combinatorics.set_family.intersecting

# 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, because a and aᶜ cannot simultaneously be in it.
• set.intersecting.is_max_iff_card_eq: Any maximal intersecting family takes up half the elements.

## References #

def set.intersecting {α : Type u_1} [order_bot α] (s : set α) :
Prop

A set family is intersecting if every pair of elements is non-disjoint.

Equations
theorem set.intersecting.mono {α : Type u_1} [order_bot α] {s t : set α} (h : t s) (hs : s.intersecting) :
theorem set.intersecting.not_bot_mem {α : Type u_1} [order_bot α] {s : set α} (hs : s.intersecting) :
theorem set.intersecting.ne_bot {α : Type u_1} [order_bot α] {s : set α} {a : α} (hs : s.intersecting) (ha : a s) :
theorem set.intersecting_empty {α : Type u_1} [order_bot α] :
@[simp]
theorem set.intersecting_singleton {α : Type u_1} [order_bot α] {a : α} :
theorem set.intersecting.insert {α : Type u_1} [order_bot α] {s : set α} {a : α} (hs : s.intersecting) (ha : a ) (h : (b : α), b s ¬ b) :
theorem set.intersecting_insert {α : Type u_1} [order_bot α] {s : set α} {a : α} :
s.intersecting a (b : α), b s ¬ b
theorem set.intersecting_iff_pairwise_not_disjoint {α : Type u_1} [order_bot α] {s : set α} :
s.intersecting s.pairwise (λ (a b : α), ¬ b) s {}
@[protected]
theorem set.subsingleton.intersecting {α : Type u_1} [order_bot α] {s : set α} (hs : s.subsingleton) :
@[protected]
theorem set.intersecting.is_upper_set {α : Type u_1} [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} [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_set {α : Type u_1} {𝒜 : set (set α)} (h𝒜 : 𝒜.intersecting) {s t : set α} (hs : s 𝒜) (ht : t 𝒜) :
(a : α), a s a t
theorem set.intersecting.exists_mem_finset {α : Type u_1} [decidable_eq α] {𝒜 : set (finset α)} (h𝒜 : 𝒜.intersecting) {s t : finset α} (hs : s 𝒜) (ht : t 𝒜) :
(a : α), a s a t
theorem set.intersecting.not_compl_mem {α : Type u_1} {s : set α} (hs : s.intersecting) {a : α} (ha : a s) :
a s
theorem set.intersecting.not_mem {α : Type u_1} {s : set α} (hs : s.intersecting) {a : α} (ha : a s) :
a s
theorem set.intersecting.disjoint_map_compl {α : Type u_1} {s : finset α} (hs : s.intersecting) :
theorem set.intersecting.card_le {α : Type u_1} [fintype α] {s : finset α} (hs : s.intersecting) :
2 * s.card
theorem set.intersecting.is_max_iff_card_eq {α : Type u_1} [nontrivial α] [fintype α] {s : finset α} (hs : s.intersecting) :
( (t : finset α), t.intersecting s t s = t) 2 * s.card =
theorem set.intersecting.exists_card_eq {α : Type u_1} [nontrivial α] [fintype α] {s : finset α} (hs : s.intersecting) :
(t : finset α), s t 2 * t.card = t.intersecting