English
If infEdist x E ≤ infEdist y E, then thickenedIndicator δ E y ≤ thickenedIndicator δ E x.
Русский
Если infEdist(x,E) ≤ infEdist(y,E), то thickenedIndicator δ E y ≤ thickenedIndicator δ E x.
LaTeX
$$$\forall δ \in \mathbb{R},\; \forall E,\; \forall x,y:\; \infEdist(x,E) ≤ \infEdist(y,E) \Rightarrow \operatorname{thickenedIndicator}(δ,E)(y) ≤ \operatorname{thickenedIndicator}(δ,E)(x)$$$
Lean4
@[gcongr]
theorem thickenedIndicator_mono_infEdist {δ : ℝ} (δ_pos : 0 < δ) {E : Set α} {x y : α}
(h : infEdist x E ≤ infEdist y E) : thickenedIndicator δ_pos E y ≤ thickenedIndicator δ_pos E x :=
by
simp only [thickenedIndicator_apply]
gcongr
· finiteness
· exact thickenedIndicatorAux_mono_infEdist δ h