le_card_infs_mul_card_sups — Mathlib

English

A lattice-based Daykin inequality: for finite α and appropriate functions, one gets a bound relating products of sums to sums over certain lattice combinations.

Русский

Неравенство Дэйкена для конечной решётки: для подходящих функций существует окольная граница между произведением сумм и суммами по комбинированным операциям на решётке.

LaTeX

$$$$\\#s\\cdot\\#t \\le \\#(s\\sqcap t)\\cdot\\#(s\\sqcup t)$$$$

Lean4

/-- An inequality of Daykin. Interestingly, any lattice in which this inequality holds is
distributive. -/
theorem le_card_infs_mul_card_sups [DecidableEq α] (s t : Finset α) : #s * #t ≤ #(s ⊼ t) * #(s ⊻ t) := by
  simpa using
    four_functions_theorem (1 : α → ℕ) 1 1 1 zero_le_one zero_le_one zero_le_one zero_le_one (fun _ _ ↦ le_rfl) s t

Похожие утверждения