English
If infEdist x E ≤ infEdist y E, then thickenedIndicatorAux δ E y ≤ thickenedIndicatorAux δ E x.
Русский
Если infEdist(x,E) ≤ infEdist(y,E), то thickenedIndicatorAux δ E y ≤ thickenedIndicatorAux δ E x.
LaTeX
$$$\forall δ \in \mathbb{R},\; \forall E \subseteq \alpha,\; \forall x,y:\; \infEdist(x,E) \le \infEdist(y,E) \Rightarrow \operatorname{thickenedIndicatorAux}(δ,E)(y) \le \operatorname{thickenedIndicatorAux}(δ,E)(x)$$$
Lean4
theorem thickenedIndicatorAux_mono_infEdist (δ : ℝ) {E : Set α} {x y : α} (h : infEdist x E ≤ infEdist y E) :
thickenedIndicatorAux δ E y ≤ thickenedIndicatorAux δ E x :=
by
simp only [thickenedIndicatorAux]
rcases le_total (infEdist x E / ENNReal.ofReal δ) 1 with hle | hle
· rw [ENNReal.sub_le_sub_iff_left hle (by simp)]
gcongr
· rw [tsub_eq_zero_of_le hle, tsub_eq_zero_of_le]
exact hle.trans (by gcongr)
