English
A prepartition of I can be built from a finite set of possibly empty boxes by discarding the empty one and preserving disjointness and below-I-constraint.
Русский
Предразбиение I можно построить из конечного множества возможно пустых коробок, удалив пустые и сохранив несовпадение и условие ниже I.
LaTeX
$$$ ofWithBot(boxes, le\_of\_mem, pairwise\_disjoint) := \\text{a Prepartition } I \\text{ with } boxes := eraseNone(boxes) \\text{ and appropriate proofs.}$$$
Lean4
/-- Create a `BoxIntegral.Prepartition` from a collection of possibly empty boxes by filtering out
the empty one if it exists. -/
def ofWithBot (boxes : Finset (WithBot (Box ι))) (le_of_mem : ∀ J ∈ boxes, (J : WithBot (Box ι)) ≤ I)
(pairwise_disjoint : Set.Pairwise (boxes : Set (WithBot (Box ι))) Disjoint) : Prepartition I
where
boxes := Finset.eraseNone boxes
le_of_mem' J
hJ := by
rw [mem_eraseNone] at hJ
simpa only [WithBot.some_eq_coe, WithBot.coe_le_coe] using le_of_mem _ hJ
pairwiseDisjoint J₁ h₁ J₂ h₂
hne := by
simp only [mem_coe, mem_eraseNone] at h₁ h₂
exact Box.disjoint_coe.1 (pairwise_disjoint h₁ h₂ (mt Option.some_inj.1 hne))
