English
If δ > 0 and x ∉ thickening δ E, then thickenedIndicatorAux δ E x = 0.
Русский
Если δ > 0 и x не принадлежит δ-толщению E, то thickenedIndicatorAux δ E x = 0.
LaTeX
$$$\forall δ \in \mathbb{R}, δ > 0,\; \forall E\subseteq \alpha,\; x\in \alpha:\; x \notin \operatorname{thickening}(δ,E) \Rightarrow \operatorname{thickenedIndicatorAux}(δ,E)(x) = 0$$$
Lean4
theorem thickenedIndicatorAux_zero {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) {x : α} (x_out : x ∉ thickening δ E) :
thickenedIndicatorAux δ E x = 0 :=
by
rw [thickening, mem_setOf_eq, not_lt] at x_out
unfold thickenedIndicatorAux
apply le_antisymm _ bot_le
have key := tsub_le_tsub (@rfl _ (1 : ℝ≥0∞)).le (ENNReal.div_le_div x_out (@rfl _ (ENNReal.ofReal δ : ℝ≥0∞)).le)
rw [ENNReal.div_self (ne_of_gt (ENNReal.ofReal_pos.mpr δ_pos)) ofReal_ne_top] at key
simpa [tsub_self] using key
