thickenedIndicator_mono_infEdist — Mathlib

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

Похожие утверждения