exists_splitMany_le — Mathlib

English

The iUnion of the complement partition π.compl equals the set difference I \\\\ π.iUnion.

Русский

Объединение iUnion дополнения разбиения π_compl равно разности I \\ π.iUnion.

LaTeX

$$$\\pi.compl.\\mathrm{iUnion} = \\uparrow I \\setminus \\pi.\\mathrm{iUnion}$$$

Lean4

/-- If `π` is a partition of `I`, then there exists a finite set `s` of hyperplanes such that
`splitMany I s ≤ π`. -/
theorem exists_splitMany_le {I : Box ι} {π : Prepartition I} (h : IsPartition π) : ∃ s, splitMany I s ≤ π :=
  by
  refine (eventually_splitMany_inf_eq_filter π).exists.imp fun s hs => ?_
  rwa [h.iUnion_eq, filter_of_true, inf_eq_right] at hs
  exact fun J hJ => le_of_mem _ hJ

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