isPartition_splitMany — Mathlib

English

SplitMany I s is a partition for any finite s.

Русский

SplitMany I s является разбиением для любого конечного множества s.

LaTeX

$$$\\mathrm{IsPartition}(\\mathrm{splitMany}\\ I\\ s)$$$

Lean4

theorem isPartition_splitMany (I : Box ι) (s : Finset (ι × ℝ)) : IsPartition (splitMany I s) := by
  classical
    exact
    Finset.induction_on s (by simp only [splitMany_empty, isPartitionTop]) fun a s _ hs => by
      simpa only [splitMany_insert, inf_split] using hs.biUnion fun J _ => isPartitionSplit _ _ _

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