splitMany_insert — Mathlib

English

Inserting one hyperplane into s splits corresponds to taking the infimum with the single-slice split by that hyperplane: splitMany I (insert p s) = splitMany I s ⊓ split I p.1 p.2.

Русский

Добавление одной гиперплоскости в s эквивалентно взятию наименьшего разбиения со вставкой разбиения по этой гиперплоскости: splitMany I (insert p s) = splitMany I s ⊓ split I p.1 p.2.

LaTeX

$$$\\mathrm{splitMany}\\ I\\ (\\mathrm{insert}\\ p\\ s) = (\\mathrm{splitMany}\\ I\\ s) \\inf (\\mathrm{split}\\ I\\ p.1\\ p.2)$$$

Lean4

@[simp]
theorem splitMany_insert (I : Box ι) (s : Finset (ι × ℝ)) (p : ι × ℝ) :
    splitMany I (insert p s) = splitMany I s ⊓ split I p.1 p.2 := by
  rw [splitMany, Finset.inf_insert, inf_comm, splitMany]

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