English
As δseq → 0, the bounded thickened indicator functions converge to the indicator of the closure E in the product topology.
Русский
Поверяйте: при δseq → 0, ограниченные функц. индикатора сходят к индикатору замыкания E в произведённой топологии.
LaTeX
$$$\text{Let } (δ_n) \to 0;\; \operatorname{thickenedIndicator}(δ_n,E) \to \mathbf{1}_{\overline{E}} \text{ in } \alpha \to \mathbb{R}_{\ge 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`.
`thickenedIndicator` is the (bundled) bounded continuous function with `ℝ≥0`-values.
See `thickenedIndicatorAux` for the unbundled `ℝ≥0∞`-valued function. -/
@[simps]
def thickenedIndicator {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) : α →ᵇ ℝ≥0
where
toFun := fun x : α => (thickenedIndicatorAux δ E x).toNNReal
continuous_toFun :=
by
apply ContinuousOn.comp_continuous continuousOn_toNNReal (continuous_thickenedIndicatorAux δ_pos E)
intro x
exact (lt_of_le_of_lt (@thickenedIndicatorAux_le_one _ _ δ E x) one_lt_top).ne
map_bounded' := by
use 2
intro x y
rw [NNReal.dist_eq]
apply (abs_sub _ _).trans
rw [NNReal.abs_eq, NNReal.abs_eq, ← one_add_one_eq_two]
have key := @thickenedIndicatorAux_le_one _ _ δ E
apply add_le_add <;>
· norm_cast
exact (toNNReal_le_toNNReal (lt_of_le_of_lt (key _) one_lt_top).ne one_ne_top).mpr (key _)
