English
ω is a symmetric fractional polymorphism for Γ iff ω is a fractional polymorphism for Γ and ω is symmetric.
Русский
ω является симметричным фракционным полиморфизмом для Γ тогда и только тогда, когда ω является фракционным полиморфизмом и симметрична.
LaTeX
$$$\\omega.IsFractionalPolymorphismFor Γ ∧ \\omega.IsSymmetric$$$
Lean4
/-- The pigeonhole principle for finitely many pigeons counted by weight, non-strict inequality
version: if the total weight of a finite set of pigeons is greater than or equal to `n • b`, they
are sorted into some pigeonholes, and for all but `n > 0` pigeonholes the total weight of the
pigeons there is nonpositive, then for at least one of these `n` pigeonholes, the total weight of
the pigeons in this pigeonhole is greater than or equal to `b`. -/
theorem exists_le_sum_fiber_of_sum_fiber_nonpos_of_nsmul_le_sum (hf : ∀ y ∉ t, ∑ x ∈ s with f x = y, w x ≤ 0)
(ht : t.Nonempty) (hb : #t • b ≤ ∑ x ∈ s, w x) : ∃ y ∈ t, b ≤ ∑ x ∈ s with f x = y, w x :=
exists_le_of_sum_le ht <|
calc
∑ _y ∈ t, b ≤ ∑ x ∈ s, w x := by simpa
_ ≤ ∑ y ∈ t, ∑ x ∈ s with f x = y, w x := sum_le_sum_fiberwise_of_sum_fiber_nonpos hf
