fin_support_approx

Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.FinStronglyMeasurable.fin_support_approx

English

For Finite Strongly Measurable f, the approximating sequence has finite support at each stage.

Русский

У последовательности приближений конечной сильной измеримости на каждом шаге конечная поддержка.

LaTeX

$$$\forall n, \mu(\mathrm{support}(f_n)) < \infty$$$

Lean4

protected theorem fin_support_approx : ∀ n, μ (support (hf.approx n)) < ∞ :=
  hf.choose_spec.1

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

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

Разделы

Аффилиация

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