isEquipartition — Mathlib

English

If the set of parts P.parts is subsingleton (i.e., there is at most one distinct part), then P is an equipartition.

Русский

Если множество частей P.parts содержит не более одной части, то P является равноправным разбиением.

LaTeX

$$(P.parts) is a Subsingleton ⇒ P.IsEquipartition$$

Lean4

theorem _root_.Set.Subsingleton.isEquipartition (h : (P.parts : Set (Finset α)).Subsingleton) : P.IsEquipartition :=
  Set.Subsingleton.equitableOn h _

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