instUniqueBot — Mathlib

English

There is a unique finpartition of ⊥, i.e., Finpartition(⊥) has a unique instance.

Русский

Существует единственное финразбиение для ⊥.

LaTeX

$$$\text{Unique}(\mathrm{Finpartition}(\bot))$$$

Lean4

instance : Unique (Finpartition (⊥ : α)) :=
  { (inferInstance : Inhabited (Finpartition (⊥ : α))) with
    uniq := fun P ↦ by
      ext a
      exact iff_of_false (fun h ↦ P.ne_bot h <| le_bot_iff.1 <| P.le h) (notMem_empty a) }
    -- See note [reducible non-instances]

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