instFintypeOfDecidableEq — Mathlib

English

If α is a lattice with bottom and there is a decidable equality on α, and α is finite, then Finpartition a is finite for any a.

Русский

Если есть булева эквивалентность на α и α конечно, то Finpartition a конечно.

LaTeX

$$$[Fintype\;\alpha] \\ [DecidableEq\;\alpha] \Rightarrow \text{Fintype}(\mathrm{Finpartition}(a))$$$

Lean4

instance [Fintype α] [DecidableEq α] (a : α) : Fintype (Finpartition a) :=
  @Fintype.ofSurjective { p : Finset α // p.SupIndep id ∧ p.sup id = a ∧ ⊥ ∉ p } (Finpartition a) _ (Subtype.fintype _)
    (fun i ↦ ⟨i.1, i.2.1, i.2.2.1, i.2.2.2⟩) fun ⟨_, y, z, w⟩ ↦ ⟨⟨_, y, z, w⟩, rfl⟩

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