comp_tendsto — Mathlib

English

If hφ is an ae-cover and u is a function with Tendsto u from l' to l, then the pullback cover hφ along u is an ae-cover for l' with φ ∘ u.

Русский

Если $h_\phi$ образует ae-покрытие и $u$ удовлетворяет условию сходства Tendsto: l' \to l, то обратно вытянутое покрытие вдоль $u$ образует ae-покрытие для $l'$ с $φ ∘ u$.

LaTeX

$$$\\forall hφ : MeasureTheory.AECover μ l φ,\\ Tendsto u l' l \\Rightarrow MeasureTheory.AECover μ l' (Function.comp φ u)$$$

Lean4

theorem comp_tendsto {α ι ι' : Type*} [MeasurableSpace α] {μ : Measure α} {l : Filter ι} {l' : Filter ι'}
    {φ : ι → Set α} (hφ : AECover μ l φ) {u : ι' → ι} (hu : Tendsto u l' l) : AECover μ l' (φ ∘ u)
    where
  ae_eventually_mem := hφ.ae_eventually_mem.mono fun _x hx => hu.eventually hx
  measurableSet i := hφ.measurableSet (u i)

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