isSubordinate_biUnionTagged — Mathlib

English

Equivalent to the previous statement, emphasizing the equivalence of Henstock property across the biUnionTagged construction.

Русский

Эквивалентно предыдущему, подчёркивая эквивалентность свойства Henstock через конструкцию biUnionTagged.

LaTeX

$$$ IsHenstock(\\pi.biUnionTagged πi) \\iff \\forall J \\in π, (π_i J).IsHenstock $$$

Lean4

@[simp]
theorem isSubordinate_biUnionTagged [Fintype ι] {π : Prepartition I} {πi : ∀ J, TaggedPrepartition J} :
    IsSubordinate (π.biUnionTagged πi) r ↔ ∀ J ∈ π, (πi J).IsSubordinate r :=
  π.forall_biUnionTagged (fun x J => Box.Icc J ⊆ closedBall x (r x)) πi

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