# mathlib3documentation

combinatorics.set_family.ahlswede_zhang

# The Ahlswede-Zhang identity #

This file proves the Ahlswede-Zhang identity, which is a nontrivial relation between the size of the "truncated unions" of a set family. It sharpens the Lubell-Yamamoto-Meshalkin inequality finset.sum_card_slice_div_choose_le_one, by making explicit the correction term.

For a set family 𝒜, the Ahlswede-Zhang identity states that the sum of |⋂ B ∈ 𝒜, B ⊆ A, B|/(|A| * n.choose |A|) is exactly 1.

## Main declarations #

• finset.truncated_sup: s.truncated_sup a is the supremum of all b ≤ a in 𝒜 if there are some, or if there are none.
• finset.truncated_inf s.truncated_inf a is the infimum of all b ≥ a in 𝒜 if there are some, or if there are none.

## References #

### Truncated supremum, truncated infimum #

def finset.truncated_sup {α : Type u_1} [order_top α] (s : finset α) (a : α) :
α

The infimum of the elements of s less than a if there are some, otherwise .

Equations
theorem finset.truncated_sup_of_mem {α : Type u_1} [order_top α] {s : finset α} {a : α} (h : a ) :
= (finset.filter (λ (b : α), a b) s).sup' _ id
theorem finset.truncated_sup_of_not_mem {α : Type u_1} [order_top α] {s : finset α} {a : α} (h : a ) :
@[simp]
theorem finset.truncated_sup_empty {α : Type u_1} [order_top α] (a : α) :
theorem finset.le_truncated_sup {α : Type u_1} [order_top α] {s : finset α} {a : α} :
a
theorem finset.map_truncated_sup {α : Type u_1} {β : Type u_2} [order_top α] (e : α ≃o β) (s : finset α) (a : α) :
e (s.truncated_sup a) = (e a)
theorem finset.truncated_sup_union {α : Type u_1} [order_top α] {s t : finset α} {a : α} [decidable_eq α] (hs : a ) (ht : a ) :
theorem finset.truncated_sup_union_left {α : Type u_1} [order_top α] {s t : finset α} {a : α} [decidable_eq α] (hs : a ) (ht : a ) :
theorem finset.truncated_sup_union_right {α : Type u_1} [order_top α] {s t : finset α} {a : α} [decidable_eq α] (hs : a ) (ht : a ) :
theorem finset.truncated_sup_union_of_not_mem {α : Type u_1} [order_top α] {s t : finset α} {a : α} [decidable_eq α] (hs : a ) (ht : a ) :
def finset.truncated_inf {α : Type u_1} (s : finset α) (a : α) :
α

The infimum of the elements of s less than a if there are some, otherwise .

Equations
theorem finset.truncated_inf_of_mem {α : Type u_1} {s : finset α} {a : α} (h : a ) :
= (finset.filter (λ (b : α), b a) s).inf' _ id
theorem finset.truncated_inf_of_not_mem {α : Type u_1} {s : finset α} {a : α} (h : a ) :
theorem finset.truncated_inf_le {α : Type u_1} (s : finset α) (a : α) :
a
@[simp]
theorem finset.truncated_inf_empty {α : Type u_1} (a : α) :
theorem finset.map_truncated_inf {α : Type u_1} {β : Type u_2} (e : α ≃o β) (s : finset α) (a : α) :
e (s.truncated_inf a) = (e a)
theorem finset.truncated_inf_union {α : Type u_1} {s t : finset α} {a : α} [decidable_eq α] (hs : a ) (ht : a ) :
theorem finset.truncated_inf_union_left {α : Type u_1} {s t : finset α} {a : α} [decidable_eq α] (hs : a ) (ht : a ) :
theorem finset.truncated_inf_union_right {α : Type u_1} {s t : finset α} {a : α} [decidable_eq α] (hs : a ) (ht : a ) :
theorem finset.truncated_inf_union_of_not_mem {α : Type u_1} {s t : finset α} {a : α} [decidable_eq α] (hs : a ) (ht : a ) :
theorem finset.truncated_sup_infs {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} (hs : a ) (ht : a ) :
theorem finset.truncated_inf_sups {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} (hs : a ) (ht : a ) :
theorem finset.truncated_sup_infs_of_not_mem {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} (ha : a ) :
theorem finset.truncated_inf_sups_of_not_mem {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} (ha : a ) :
@[simp]
theorem finset.compl_truncated_sup {α : Type u_1} (s : finset α) (a : α) :
@[simp]
theorem finset.compl_truncated_inf {α : Type u_1} (s : finset α) (a : α) :
theorem finset.card_truncated_sup_union_add_card_truncated_sup_infs {α : Type u_1} [decidable_eq α] [fintype α] (𝒜 ℬ : finset (finset α)) (s : finset α) :
((𝒜 ℬ).truncated_sup s).card + ((𝒜 ℬ).truncated_sup s).card = (𝒜.truncated_sup s).card + (ℬ.truncated_sup s).card