mathlib3 documentation

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 #

References #

def set.intersecting {α : Type u_1} [semilattice_inf α] [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} [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 : α} :
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 : α} :
theorem set.intersecting_iff_pairwise_not_disjoint {α : Type u_1} [semilattice_inf α] [order_bot α] {s : set α} :
s.intersecting s.pairwise (λ (a b : α), ¬disjoint a b) s {}
@[protected]
theorem set.subsingleton.intersecting {α : Type u_1} [semilattice_inf α] [order_bot α] {s : set α} (hs : s.subsingleton) :
@[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_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} [boolean_algebra α] {s : set α} (hs : s.intersecting) {a : α} (ha : a s) :
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.card_le {α : Type u_1} [boolean_algebra α] [fintype α] {s : finset α} (hs : s.intersecting) :
theorem set.intersecting.is_max_iff_card_eq {α : Type u_1} [boolean_algebra α] [nontrivial α] [fintype α] {s : finset α} (hs : s.intersecting) :
( (t : finset α), t.intersecting s t s = t) 2 * s.card = fintype.card α