English
Let E be a normed abelian group over ℝ with a real δ > 0 and any set s ⊆ E. Then infEdist x (thickening δ s) = infEdist x s − ENNReal.ofReal δ for every x ∈ E.
Русский
Пусть E — нормированная абелева группа над ℝ, δ>0 и любой набор s ⊆ E. Тогда infEdist x (thickening δ s) = infEdist x s − ENNReal.ofReal δ для каждого x ∈ E.
LaTeX
$$$$\forall x\in E:\; \operatorname{infEdist}(x, \operatorname{thickening}(\delta, s)) = \operatorname{infEdist}(x, s) - \operatorname{ENNReal}.ofReal(\delta). $$$$
Lean4
@[simp]
theorem infEdist_thickening (hδ : 0 < δ) (s : Set E) (x : E) :
infEdist x (thickening δ s) = infEdist x s - ENNReal.ofReal δ :=
by
obtain hs | hs := lt_or_ge (infEdist x s) (ENNReal.ofReal δ)
· rw [infEdist_zero_of_mem, tsub_eq_zero_of_le hs.le]
exact hs
refine (tsub_le_iff_right.2 infEdist_le_infEdist_thickening_add).antisymm' ?_
refine le_sub_of_add_le_right ofReal_ne_top ?_
refine le_infEdist.2 fun z hz => le_of_forall_gt fun r h => ?_
cases r with
| top =>
exact add_lt_top.2 ⟨lt_top_iff_ne_top.2 <| infEdist_ne_top ⟨z, self_subset_thickening hδ _ hz⟩, ofReal_lt_top⟩
| coe
r =>
have hr : 0 < ↑r - δ := by
refine sub_pos_of_lt ?_
have := hs.trans_lt ((infEdist_le_edist_of_mem hz).trans_lt h)
rw [ofReal_eq_coe_nnreal hδ.le] at this
exact mod_cast this
rw [edist_lt_coe, ← dist_lt_coe, ← add_sub_cancel δ ↑r] at h
obtain ⟨y, hxy, hyz⟩ := exists_dist_lt_lt hr hδ h
refine
(ENNReal.add_lt_add_right ofReal_ne_top <|
infEdist_lt_iff.2 ⟨_, mem_thickening_iff.2 ⟨_, hz, hyz⟩, edist_lt_ofReal.2 hxy⟩).trans_le
?_
rw [← ofReal_add hr.le hδ.le, sub_add_cancel, ofReal_coe_nnreal]
