parts_top_subset — Mathlib

English

For a fixed a, the top finpartition's parts are contained in the singleton {a} (under decidable equality).

Русский

Верхнее разбиение имеет блоки, лежащие внутри множества {a} при допускаемом равенстве.

LaTeX

$$$((\top : \mathrm{Finpartition}(a)).\text{parts}) \subseteq \{a\}$$$

Lean4

theorem parts_top_subset (a : α) [Decidable (a = ⊥)] : (⊤ : Finpartition a).parts ⊆ { a } :=
  by
  intro b hb
  have hb : b ∈ Finpartition.parts (dite _ _ _) := hb
  split_ifs at hb
  · simp only [copy_parts, empty_parts, notMem_empty] at hb
  · exact hb

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