English
There exists a Finpartition of s built from given parts, provided that (i) each p ∈ parts satisfies p ⊆ s, (ii) every a ∈ s lies in exactly one p ∈ parts, and (iii) ∅ ∉ parts.
Русский
Существует Finpartition s, построенный из заданной коллекции частей, если выполняются условия (i)–(iii).
LaTeX
$$$ \exists P : Finpartition s, \ (\forall p \in parts, p \subseteq s) \land (\forall a \in s, \exists! t \in parts, a \in t) \land (∅ \notin parts) $$$
Lean4
/-- Construct a `Finpartition s` from a finset of finsets `parts` such that each element of `s` is in
exactly one member of `parts`. This provides a converse to `Finpartition.subset`,
`Finpartition.not_empty_mem_parts` and `Finpartition.existsUnique_mem`.
-/
@[simps]
def ofExistsUnique (parts : Finset (Finset α)) (h : ∀ p ∈ parts, p ⊆ s) (h' : ∀ a ∈ s, ∃! t ∈ parts, a ∈ t)
(h'' : ∅ ∉ parts) : Finpartition s where
parts := parts
supIndep := by
simp only [supIndep_iff_pairwiseDisjoint]
intro a ha b hb hab
rw [Function.onFun, Finset.disjoint_left]
intro x hx hx'
exact hab ((h' x (h _ ha hx)).unique ⟨ha, hx⟩ ⟨hb, hx'⟩)
sup_parts := by
ext i
simp only [mem_sup, id_eq]
constructor
· rintro ⟨j, hj, hj'⟩
exact h j hj hj'
· rintro hi
exact (h' i hi).exists
bot_notMem := h''
