biUnionTagged

Mathlib.Analysis.BoxIntegral.Partition.Tagged

URI: https://scilib.ai/kg/mathlib#BoxIntegral.Prepartition.biUnionTagged

Lean4

/-- Given a partition `π` of `I : BoxIntegral.Box ι` and a collection of tagged partitions
`πi J` of all boxes `J ∈ π`, returns the tagged partition of `I` into all the boxes of `πi J`
with tags coming from `(πi J).tag`. -/
def biUnionTagged (π : Prepartition I) (πi : ∀ J : Box ι, TaggedPrepartition J) : TaggedPrepartition I
    where
  toPrepartition := π.biUnion fun J => (πi J).toPrepartition
  tag J := (πi (π.biUnionIndex (fun J => (πi J).toPrepartition) J)).tag J
  tag_mem_Icc _ := Box.le_iff_Icc.1 (π.biUnionIndex_le _ _) ((πi _).tag_mem_Icc _)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru