inf_splitMany — Mathlib

English

For a prepartition π and a finite s, π ⊓ splitMany I s equals the biUnion over J of splitMany J s.

Русский

Для предразбиения π и конечного s выполняется: π ⊓ splitMany I s = π.biUnion (splitMany J s).

LaTeX

$$$\\pi \\inf splitMany\\ I\\ s = \\pi\\ biUnion (\\lambda J, splitMany\\ J\\ s)$$$

Lean4

theorem inf_splitMany {I : Box ι} (π : Prepartition I) (s : Finset (ι × ℝ)) :
    π ⊓ splitMany I s = π.biUnion fun J => splitMany J s := by
  classical
    induction s using Finset.induction_on with
  | empty => simp
  | insert p s _ ihp => simp_rw [splitMany_insert, ← inf_assoc, ihp, inf_split, biUnion_assoc]

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