exists_iUnion_eq_diff — Mathlib

English

For every partition π there exists a π' with iUnion equal to the set difference I \\ π.iUnion.

Русский

Для каждого разбиения найдется π' такое, что π'.iUnion = I \\ π.iUnion.

LaTeX

$$$\\exists \\pi' : Prepartition I,\\ \\pi'.\\mathrm{iUnion} = \\uparrow I \\setminus \\pi.\\mathrm{iUnion}$$$

Lean4

/-- For every prepartition `π` of `I` there exists a prepartition that covers exactly
`I \ π.iUnion`. -/
theorem exists_iUnion_eq_diff (π : Prepartition I) : ∃ π' : Prepartition I, π'.iUnion = ↑I \ π.iUnion :=
  by
  rcases π.eventually_splitMany_inf_eq_filter.exists with ⟨s, hs⟩
  use (splitMany I s).filter fun J => ¬(J : Set (ι → ℝ)) ⊆ π.iUnion
  simp [← hs]

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