single — Mathlib

English

A tagged prepartition with a single box J, contained in I, is defined by specifying the tag value x within J, yielding a one-box tagged prepartition of I.

Русский

Тэггированное предразбиение с одним коробом J внутри I задаётся значением метки x, лежащим внутри Icc(I), образуя одночастное тэгированное предразбиение.

LaTeX

$$$\\text{single}(I,J, h_J, x, h) :\\; \\text{TaggedPrepartition } I$$$

Lean4

/-- Tagged prepartition with single box and prescribed tag. -/
@[simps! -fullyApplied]
def single (I J : Box ι) (hJ : J ≤ I) (x : ι → ℝ) (h : x ∈ Box.Icc I) : TaggedPrepartition I :=
  ⟨Prepartition.single I J hJ, fun _ => x, fun _ => h⟩

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