scalingScaleOf_pos

Mathlib.MeasureTheory.Measure.Doubling

URI: https://scilib.ai/kg/mathlib#IsUnifLocDoublingMeasure.scalingScaleOf_pos

English

For any K, scalingScaleOf μ K is strictly positive.

Русский

Для любого K величина scalingScaleOf μ K положительна.

LaTeX

$$$$ 0 < \\mathrm{scalingScaleOf}(\\mu,K). $$$$

Lean4

theorem scalingScaleOf_pos (K : ℝ) : 0 < scalingScaleOf μ K :=
  (eventually_measure_mul_le_scalingConstantOf_mul μ K).choose_spec.1

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

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

Разделы

Аффилиация

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