mem_ae_of_mem_ae_map

Mathlib.MeasureTheory.Measure.Map

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

← MathLib Explorer

English

If s ∈ ae(μ.map f), then f^{-1}(s) ∈ ae μ.

Русский

Если s принадлежит ae(μ.map f), то f^{-1}(s) принадлежит ae μ.

LaTeX

$$$ s \in ae (\mu.map f) \Rightarrow f^{-1}(s) \in ae \mu $$$

Lean4

theorem mem_ae_of_mem_ae_map {f : α → β} (hf : AEMeasurable f μ) {s : Set β} (hs : s ∈ ae (μ.map f)) : f ⁻¹' s ∈ ae μ :=
  (tendsto_ae_map hf).eventually hs

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

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

Разделы

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

Аффилиация

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