Theorems · Theorem · order theory

four_functions_theorem_univ

∀ {α : Type u_1} {β : Type u_2} [inst : DistribLattice α] [inst_1 : CommSemiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] [ExistsAddOfLE β] (f₁ f₂ f₃ f₄ : α → β) [inst_5 : Fintype α],
  0 ≤ f₁ →
    0 ≤ f₂ →
      0 ≤ f₃ →
        0 ≤ f₄ →
          (∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)) → (∑ a, f₁ a) * ∑ a, f₂ a ≤ (∑ a, f₃ a) * ∑ a, f₄ a

Special case of the Four Functions Theorem when s = t = univ.

Defined in

Mathlib.Combinatorics.SetFamily.FourFunctions

Cited by

1 results in Mathlib

Foundations

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

Assumes

DistribLatticeCommSemiringLinearOrderIsStrictOrderedRingExistsAddOfLEFintype