continuous_indicatorConstLp_set — Mathlib

English

Under mild assumptions, the map x ↦ indicatorConstLp p (hs x) (hμs x) c is continuous in x.

Русский

При умеренных предположениях отображение индикатора непрерывно по параметру x.

LaTeX

$$$x \mapsto indicatorConstLp(p, hs(x), hμs(x), c)$ is continuous.$$

Lean4

/-- A family of `indicatorConstLp` functions is continuous in the parameter,
if `μ (s y ∆ s x)` tends to zero as `y` tends to `x` for all `x`. -/
theorem continuous_indicatorConstLp_set [Fact (1 ≤ p)] {X : Type*} [TopologicalSpace X] {s : X → Set α}
    {hs : ∀ x, MeasurableSet (s x)} {hμs : ∀ x, μ (s x) ≠ ∞} (hp : p ≠ ∞)
    (h : ∀ x, Tendsto (fun y ↦ μ (s y ∆ s x)) (𝓝 x) (𝓝 0)) : Continuous fun x ↦ indicatorConstLp p (hs x) (hμs x) c :=
  continuous_iff_continuousAt.2 fun x ↦ tendsto_indicatorConstLp_set hp (h x)

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