English
For any δ > 0, thickenedIndicatorAux δ E is a continuous function on α.
Русский
Для любого δ > 0 функция thickenedIndicatorAux δ E непрерывна на α.
LaTeX
$$$\\text{continuous_thickenedIndicatorAux}(δ,E):\\; α \\to \\mathbb{R}_{\\ge 0}^{\\infty}$ is continuous for δ > 0.$$
Lean4
/-- The `δ`-thickened indicator of a set `E` is the function that equals `1` on `E`
and `0` outside a `δ`-thickening of `E` and interpolates (continuously) between
these values using `infEdist _ E`.
`thickenedIndicatorAux` is the unbundled `ℝ≥0∞`-valued function. See `thickenedIndicator`
for the (bundled) bounded continuous function with `ℝ≥0`-values. -/
def thickenedIndicatorAux (δ : ℝ) (E : Set α) : α → ℝ≥0∞ := fun x : α => (1 : ℝ≥0∞) - infEdist x E / ENNReal.ofReal δ
