indiscrete_isEquipartition — Mathlib

English

For a nonempty finite set s, the indiscrete partition of s is equipartition.

Русский

Для непустого множества s индиспремное разбиение множества s является равномерным разбиением.

LaTeX

$$$ (s \\neq \\emptyset) \\Rightarrow \\mathrm{IsEquipartition}(\\mathrm{indiscrete}(s))$$$

Lean4

theorem indiscrete_isEquipartition {hs : s ≠ ∅} : (indiscrete hs).IsEquipartition :=
  by
  rw [IsEquipartition, indiscrete_parts, coe_singleton]
  exact Set.equitableOn_singleton s _

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