IsSubordinate — Mathlib

English

A tagged prepartition is Henstock with respect to r if and only if each J in the underlying partition π is Henstock under r.

Русский

Тэггированное предразбиение являетсяHenstock по r тогда, когда каждая коробка J в основании разбиения π удовлетворяет Henstock по r.

LaTeX

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

Lean4

/-- A tagged partition `π` is subordinate to `r : (ι → ℝ) → ℝ` if each box `J ∈ π` is included in
the closed ball with center `π.tag J` and radius `r (π.tag J)`. -/
def IsSubordinate [Fintype ι] (π : TaggedPrepartition I) (r : (ι → ℝ) → Ioi (0 : ℝ)) : Prop :=
  ∀ J ∈ π, Box.Icc J ⊆ closedBall (π.tag J) (r <| π.tag J)

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