not_isEquipartition — Mathlib

English

A Finpartition is not equipartition if and only if there exist two parts with sizes violating the equal-sizes condition (one larger by more than 1).

Русский

Финразбиение неравноправно тогда и только тогда, когда существуют две части с различиями в размерах, превышающими 1.

LaTeX

$$¬P.IsEquipartition \iff ∃ a,b ∈ P.parts, #b + 1 < #a$$

Lean4

theorem not_isEquipartition : ¬P.IsEquipartition ↔ ∃ a ∈ P.parts, ∃ b ∈ P.parts, #b + 1 < #a :=
  Set.not_equitableOn

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