parts_top_subsingleton — Mathlib

English

The set of blocks of the top finpartition is a singleton when a ≠ ⊥ and decidable equality holds.

Русский

Множество блоков верхнего разбиения является синглетоном при выполнении условий.

LaTeX

$$$((\top : \mathrm{Finpartition}(a)).\text{parts} : \mathrm{Set} \alpha).\mathrm{Subsingleton}$$$

Lean4

theorem parts_top_subsingleton (a : α) [Decidable (a = ⊥)] : ((⊤ : Finpartition a).parts : Set α).Subsingleton :=
  Set.subsingleton_of_subset_singleton fun _ hb ↦ mem_singleton.1 <| parts_top_subset _ hb

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