parts_bot — Mathlib

English

As above, the bottom partition of s has exactly the singleton blocks, i.e., equals the image of s under the singleton map.

Русский

Как и выше, нижнее разбиение s состоит из одинарных блоков; это равносильно образу s под отображением, отправляющим элемента в его одинарное множество.

LaTeX

$$$ (\\perp_{Finpartition(s)}).{\\rm parts} = s.{\\rm image}(\\\\text{singleton})$$

Lean4

@[simp]
theorem parts_bot (s : Finset α) : (⊥ : Finpartition s).parts = s.map ⟨singleton, singleton_injective⟩ :=
  rfl

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