iUnionUpTo

Mathlib.MeasureTheory.Covering.Besicovitch

URI: https://scilib.ai/kg/mathlib#Besicovitch.TauPackage.iUnionUpTo

Lean4

/-- The set of points that are covered by the union of balls selected at steps `< i`. -/
def iUnionUpTo (i : Ordinal.{u}) : Set α :=
  ⋃ j : { j // j < i }, ball (p.c (p.index j)) (p.r (p.index j))

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

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

Разделы

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

Аффилиация

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