English
GaugeRescale is continuous under the standard topological hypotheses (convex, absorbent sets with 0 in interior, von Neumann boundedness).
Русский
Гейдж-скейл непрерывен при стандартных топологических условиях (выпуклость, абсорбентность,Von Neumann ограниченность и т.д.).
LaTeX
$$Continuous (gaugeRescale s t) under given hypotheses$$
Lean4
theorem continuous_gaugeRescale {s t : Set E} (hs : Convex ℝ s) (hs₀ : s ∈ 𝓝 0) (ht : Convex ℝ t) (ht₀ : t ∈ 𝓝 0)
(htb : IsVonNBounded ℝ t) : Continuous (gaugeRescale s t) :=
by
have hta : Absorbent ℝ t := absorbent_nhds_zero ht₀
refine continuous_iff_continuousAt.2 fun x ↦ ?_
rcases eq_or_ne x 0 with rfl | hx
· rw [ContinuousAt, gaugeRescale_zero]
nth_rewrite 2 [← comap_gauge_nhds_zero htb ht₀]
simp only [tendsto_comap_iff, Function.comp_def, gauge_gaugeRescale _ hta htb]
exact tendsto_gauge_nhds_zero hs₀
·
exact
((continuousAt_gauge hs hs₀).div (continuousAt_gauge ht ht₀) ((gauge_pos hta htb).2 hx).ne').smul continuousAt_id
