top_isEquipartition — Mathlib

English

The top finpartition of a finite set is equipartition (under suitable decidability assumptions).

Русский

Верхнее разбиение Finpartition является равномерным при надлежащих предпосылках о разрешимости равенств.

LaTeX

$$$ \\text{IsEquipartition}(\\top_{\\mathrm{Finpartition}(s)})$$$

Lean4

theorem top_isEquipartition [Decidable (s = ⊥)] : (⊤ : Finpartition s).IsEquipartition :=
  Set.Subsingleton.isEquipartition (parts_top_subsingleton _)

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