mono_pre

Mathlib.MeasureTheory.Measure.Hausdorff

URI: https://scilib.ai/kg/mathlib#MeasureTheory.OuterMeasure.mkMetric'.mono_pre

English

The map k ↦ pre m k⁻¹ is monotone on natural numbers.

Русский

Функция k ↦ pre m k⁻¹ — монотонна по натуральным числам.

LaTeX

$$$\\text{Monotone } (\\lambda k: \\mathrm{pre}\\, m\\, k^{-1})$$$

Lean4

theorem mono_pre (m : Set X → ℝ≥0∞) {r r' : ℝ≥0∞} (h : r ≤ r') : pre m r' ≤ pre m r :=
  le_pre.2 fun _ hs => pre_le (hs.trans h)

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

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

Разделы

Аффилиация

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