unitBallPackage

Mathlib.MeasureTheory.Covering.Besicovitch

URI: https://scilib.ai/kg/mathlib#Besicovitch.unitBallPackage

Lean4

/-- The ball package made of unit balls. -/
def unitBallPackage (α : Type*) : BallPackage α α where
  c := id
  r _ := 1
  rpos _ := zero_lt_one
  r_bound := 1
  r_le _ := le_rfl

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

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

Разделы

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

Аффилиация

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