English
If a is an atom, there is a unique finpartition of a; the indiscrete partition is the default, and any finpartition is equal to it.
Русский
Если a — атом, существует единственное финразбиение a; как правило, это indiscrete-разбиение.
LaTeX
$$$\text{IsAtom}(a) \Rightarrow \mathrm{Unique}(\mathrm Finpartition}(a))$$$
Lean4
/-- There's a unique partition of an atom. -/
abbrev _root_.IsAtom.uniqueFinpartition (ha : IsAtom a) : Unique (Finpartition a)
where
default := indiscrete ha.1
uniq
P := by
have h : ∀ b ∈ P.parts, b = a := fun _ hb ↦ (ha.le_iff.mp <| P.le hb).resolve_left (P.ne_bot hb)
ext b
refine Iff.trans ⟨h b, ?_⟩ mem_singleton.symm
rintro rfl
obtain ⟨c, hc⟩ := P.parts_nonempty ha.1
simp_rw [← h c hc]
exact hc
