tendsto_smul_ae

Mathlib.MeasureTheory.Group.Action

URI: https://scilib.ai/kg/mathlib#MeasureTheory.tendsto_smul_ae

← MathLib Explorer

English

The map x ↦ c • x sends almost-everywhere convergence to itself under μ.

Русский

Отображение x ↦ c • x сохраняет AE-сходимость μ.

LaTeX

$$$\text{Tendsto}(c\cdot\,\cdot)\; (\ae\mu)\; (\ae\mu)$$$

Lean4

/-- See also `smul_ae`. -/
@[to_additive /-- See also `vadd_ae`. -/
    ]
theorem tendsto_smul_ae (c : G) : Filter.Tendsto (c • ·) (ae μ) (ae μ) := fun _s hs ↦
  eq_bot_mono (measure_preimage_smul_le μ c _) hs

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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