English
A precise technical statement asserting continuity of thickenedIndicatorAux with δ-pos condition; the proof uses continuousNNReal-sub and continuous_infEdist.
Русский
Точное техническое утверждение о непрерывности thickenedIndicatorAux при δ > 0; доказательство использует непрерывность под и инфEdist.
LaTeX
$$$\\text{continuous_thickenedIndicatorAux}(δ,E): α \\to \\mathbb{R}_{\\ge 0}^{\\infty}$ is continuous for δ > 0.$$
Lean4
theorem continuous_thickenedIndicatorAux {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) : Continuous (thickenedIndicatorAux δ E) :=
by
unfold thickenedIndicatorAux
let f := fun x : α => (⟨1, infEdist x E / ENNReal.ofReal δ⟩ : ℝ≥0 × ℝ≥0∞)
let sub := fun p : ℝ≥0 × ℝ≥0∞ => (p.1 : ℝ≥0∞) - p.2
rw [show (fun x : α => (1 : ℝ≥0∞) - infEdist x E / ENNReal.ofReal δ) = sub ∘ f by rfl]
apply (@ENNReal.continuous_nnreal_sub 1).comp
apply (ENNReal.continuous_div_const (ENNReal.ofReal δ) _).comp continuous_infEdist
norm_num [δ_pos]
