tendsto_eval_ae_ae

Mathlib.MeasureTheory.Constructions.Pi

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.tendsto_eval_ae_ae

English

For each i, the evaluation map is a.tendsto from ae(π μ) to ae(μ_i).

Русский

Для каждого i отображение вычисления является переходом от ae(π μ) к ae( μ_i ).

LaTeX

$$$\mathrm{tendsto}\ (\mathrm{eval}_i)\ (\mathrm{ae}(\pi\mu))\ (\mathrm{ae}(\mu_i))$$$

Lean4

theorem tendsto_eval_ae_ae {i : ι} : Tendsto (eval i) (ae (Measure.pi μ)) (ae (μ i)) := fun _ hs =>
  pi_eval_preimage_null μ hs

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

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

Разделы

Аффилиация

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