lowerSemicontinuous_uniformOn — Mathlib

English

The map f ↦ eVariationOn f s is lower semicontinuous with respect to uniform convergence on s.

Русский

Отображение f ↦ eVariationOn f s сохраняет нижнюю полупостоянность при равномерном сходстве на s.

LaTeX

$$$\text{LowerSemicontinuous}(f \mapsto eVariationOn f s)\text{ for uniform convergence on } s$$$

Lean4

/-- The map `(eVariationOn · s)` is lower semicontinuous for uniform convergence on `s`. -/
theorem lowerSemicontinuous_uniformOn (s : Set α) : LowerSemicontinuous fun f : α →ᵤ[{ s }] E => eVariationOn f s :=
  fun f ↦ by
  apply @lowerSemicontinuous_aux _ _ _ _ (UniformOnFun α E { s }) id (𝓝 f) f s _
  have := @tendsto_id _ (𝓝 f)
  rw [UniformOnFun.tendsto_iff_tendstoUniformlyOn] at this
  simp_rw [← tendstoUniformlyOn_singleton_iff_tendsto]
  exact fun x xs => (this s rfl).mono (singleton_subset_iff.mpr xs)

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