English
From a Finpartition P of a, one can form a Finpartition of b by selecting a subset of parts of P whose supremum is b.
Русский
Из разбиения Finpartition P множества a можно получить разбиение Finpartition b, выбрав подмножество частей разбиения P так, чтобы их наибольший элемент равнялся b.
LaTeX
$$$\\text{ofSubset}(P, \\text{subset}, \\text{sup\_parts}) : \\mathrm{Finpartition} b$$$
Lean4
/-- A `Finpartition` constructor from a bigger existing finpartition. -/
@[simps]
def ofSubset {a b : α} (P : Finpartition a) {parts : Finset α} (subset : parts ⊆ P.parts)
(sup_parts : parts.sup id = b) : Finpartition b :=
{ parts := parts
supIndep := P.supIndep.subset subset
sup_parts := sup_parts
bot_notMem := fun h ↦ P.bot_notMem (subset h) }
