Theorems · Theorem · order theory

collapse_modular

∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {a : α} {f₁ f₂ f₃ f₄ : Finset α → β} {u : Finset α} [ExistsAddOfLE β],
  a ∉ u →
    0 ≤ f₁ →
      0 ≤ f₂ →
        0 ≤ f₃ →
          0 ≤ f₄ →
            (∀ ⦃s : Finset α⦄,
                s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)) →
              ∀ (𝒜 ℬ : Finset (Finset α)) ⦃s : Finset α⦄,
                s ⊆ u →
                  ∀ ⦃t : Finset α⦄,
                    t ⊆ u →
                      collapse✝ 𝒜 a f₁ s * collapse✝ ℬ a f₂ t ≤
                        collapse✝ (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse✝ (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Defined in

Mathlib.Combinatorics.SetFamily.FourFunctions

Cited by

1 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqCommSemiringLinearOrderIsStrictOrderedRingExistsAddOfLE