prepartition_isPartition — Mathlib

English

If B has integral vertices, then the prepartition n B is a partition of B.

Русский

Если у коробки B есть интегральные вершины, то prepartition n B является разбиением B.

LaTeX

$$$$ (prepartition\ n\ B).IsPartition $$$$

Lean4

/-- If `B : BoxIntegral.Box` has integral vertices, then `prepartition n B` is a partition of
`B`. -/
theorem prepartition_isPartition {B : Box ι} (hB : hasIntegralVertices B) : (prepartition n B).IsPartition :=
  by
  refine fun x hx ↦ ⟨box n (index n x), ?_, mem_box_iff_index.mpr rfl⟩
  rw [TaggedPrepartition.mem_toPrepartition, mem_prepartition_iff]
  exact ⟨index n x, mem_admissibleIndex_of_mem_box n hB hx, rfl⟩

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