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)