distortion

Mathlib.Analysis.BoxIntegral.Partition.Tagged

URI: https://scilib.ai/kg/mathlib#BoxIntegral.TaggedPrepartition.distortion

English

Another simp-variant of IsHenstock.disjUnion.

Русский

Еще один вариант упрощения IsHenstock.disjUnion.

LaTeX

$$$ IsHenstock(π_1.disjUnion π_2 h) \text{ (simp_1) } $$$

Lean4

/-- The distortion of a tagged prepartition is the maximum of distortions of its boxes. -/
def distortion : ℝ≥0 :=
  π.toPrepartition.distortion

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

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

Разделы

Аффилиация

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