prepartition_isHenstock — Mathlib

English

For any box B, the partition (prepartition n B) satisfies the Henstock condition, i.e., it is a Henstock partition of B.

Русский

Для любых B разбиение (prepartition n B) удовлетворяет условию Хенштоука: это разбиение Хенштоука коробки B.

LaTeX

$$$$ \bigl(\mathrm{prepartition}(n,B)\bigr).\mathrm{IsHenstock}, $$$$

Lean4

theorem prepartition_isHenstock (B : Box ι) : (prepartition n B).IsHenstock :=
  by
  intro _ hI
  obtain ⟨ν, hν, rfl⟩ := mem_prepartition_iff.mp hI
  rw [prepartition_tag n hν]
  exact Box.coe_subset_Icc (tag_mem _ _)

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