instUniqueOne — Mathlib

English

There exists a unique OrderedFinpartition 1.

Русский

Существует уникальное OrderedFinpartition(1).

LaTeX

$$$\\exists! c: \\mathrm{OrderedFinpartition}(1)$$$

Lean4

instance instUniqueOne : Unique (OrderedFinpartition 1) where
  uniq
    c := by
    have h₁ : c.length = 1 := le_antisymm c.length_le (c.length_pos Nat.zero_lt_one)
    have h₂ (i) : c.partSize i = 1 := le_antisymm (c.partSize_le _) (c.partSize_pos _)
    have h₃ (i j) : c.emb i j = 0 := Subsingleton.elim _ _
    rcases c with ⟨length, partSize, _, emb, _, _, _, _⟩
    subst h₁
    obtain rfl : partSize = fun _ ↦ 1 := funext h₂
    simpa [OrderedFinpartition.ext_iff, funext_iff, Fin.forall_fin_one] using h₃ _ _

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