admissibleIndex — Mathlib

English

The set of ν such that box n ν ⊆ B is finite, and those ν form an admissible index of B.

Русский

Множество ν, для которого box n ν ⊆ B, конечно и образует допустимый индекс B.

LaTeX

$$$\mathrm{admissibleIndex}(n,B)$ is finite and equals {ν : box n ν ⊆ B}$$

Lean4

/-- For `B : BoxIntegral.Box`, the set of indices of `unitPartition.box` that are subsets of `B`.
This is a finite set. These boxes cover `B` if it has integral vertices, see
`unitPartition.prepartition_isPartition`. -/
def admissibleIndex (B : Box ι) : Finset (ι → ℤ) :=
  by
  refine (setFinite_index n B.measurableSet_coe.nullMeasurableSet ?_).toFinset
  exact lt_top_iff_ne_top.mp (IsBounded.measure_lt_top B.isBounded)

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