Positive difference

This file defines the positive difference of set families and sets in an ordered additive group.

Main declarations

• Finset.posDiffs: Positive difference of set families.
• Finset.posSub: Positive difference of sets in an ordered additive group.

Notations

We declare the following notation in the finset_family locale:

• s \₊ t for finset.posDiffs s t
• s -₊ t for finset.posSub s t

References

• [Bollobás, Leader, Radcliffe, *Reverse Kleitman Inequalities][bollobasleaderradcliffe1989]

Positive set difference

def Finset.posDiffs {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [DecidableEq α] (s t : Finset α) : Finset α

The positive set difference of finsets s and t is the set of a \ b for a ∈ s, b ∈ t, b ≤ a.

Equations

• s.posDiffs t = Finset.image (fun (x : α × α) => match x with | (a, b) => a \ b) ({x ∈ s ×ˢ t | match x with | (a, b) => b ≤ a})

def FinsetFamily.«term_\₊_» : Lean.TrailingParserDescr

Equations

• FinsetFamily.«term_\₊_» = Lean.ParserDescr.trailingNode `FinsetFamily.«term_\₊_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " \\₊ ") (Lean.ParserDescr.cat `term 71))

@[simp]

theorem Finset.mem_posDiffs {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [DecidableEq α] {s t : Finset α} {a : α} : a ∈ s.posDiffs t ↔ ∃ b ∈ s, ∃ c ∈ t, c ≤ b ∧ b \ c = a

@[simp]

theorem Finset.posDiffs_empty {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [DecidableEq α] (s : Finset α) : s.posDiffs ∅ = ∅

@[simp]

theorem Finset.empty_posDiffs {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [DecidableEq α] (s : Finset α) : ∅.posDiffs s = ∅

theorem Finset.posDiffs_subset_diffs {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [DecidableEq α] {s t : Finset α} : s.posDiffs t ⊆ s.diffs t

theorem Finset.card_posDiffs_self_le {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} (h𝒜 : (↑𝒜).OrdConnected) : (𝒜.posDiffs 𝒜).card ≤ 𝒜.card

theorem Finset.le_card_upper_inter_lower {α : Type u_1} [DecidableEq α] {𝒜 ℬ : Finset (Finset α)} (h𝒜 : IsLowerSet ↑𝒜) (hℬ : IsUpperSet ↑ℬ) : (𝒜.posDiffs ℬ).card ≤ (𝒜 ∩ ℬ).card

A reverse Kleitman inequality.

Positive subtraction

def Finset.posSub {α : Type u_1} [Sub α] [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [DecidableEq α] (s t : Finset α) : Finset α

The positive subtraction of finsets s and t is the set of a - b for a ∈ s, b ∈ t, b ≤ a.

Equations

• s.posSub t = Finset.image (fun (x : α × α) => match x with | (a, b) => a - b) ({x ∈ s ×ˢ t | match x with | (a, b) => b ≤ a})

def FinsetFamily.«term_-₊_» : Lean.TrailingParserDescr

Equations

• FinsetFamily.«term_-₊_» = Lean.ParserDescr.trailingNode `FinsetFamily.«term_-₊_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " -₊ ") (Lean.ParserDescr.cat `term 71))

theorem Finset.mem_posSub {α : Type u_1} [Sub α] [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [DecidableEq α] {s t : Finset α} {a : α} : a ∈ s.posSub t ↔ ∃ b ∈ s, ∃ c ∈ t, c ≤ b ∧ b - c = a

theorem Finset.posSub_subset_sub {α : Type u_1} [Sub α] [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [DecidableEq α] {s t : Finset α} : s.posSub t ⊆ s - t

theorem Finset.card_posSub_self_le {α : Type u_1} [Sub α] [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [DecidableEq α] {s : Finset α} (hs : (↑s).OrdConnected) : (s.posSub s).card ≤ s.card