English
Let K be compact in α and U open in β, with f: α→β continuous at every x∈K and maps K into U. Then there exists ε>0 and V in nhdsˢ K such that thickening ε of f''V is contained in U.
Русский
Пусть K компактно в α, U открыто в β, f: α→β так, что для каждого x∈K непрерывно в f(x) и f(K)⊆U. Тогда существует ε>0 и V ∈ nhdsˢ K, такое что thickening ε(f''V) ⊆ U.
LaTeX
$$$\exists ε>0,\exists V∈𝓝^{s} K\;\text{such that}\; \operatorname{thickening}_{ε}(f''V) ⊆ U$$$
Lean4
/-- For the equality, see `infEdist_cthickening`. -/
theorem infEdist_le_infEdist_cthickening_add : infEdist x s ≤ infEdist x (cthickening δ s) + ENNReal.ofReal δ :=
by
refine le_of_forall_gt fun r h => ?_
simp_rw [← lt_tsub_iff_right, infEdist_lt_iff, mem_cthickening_iff] at h
obtain ⟨y, hy, hxy⟩ := h
exact
infEdist_le_edist_add_infEdist.trans_lt
((ENNReal.add_lt_add_of_lt_of_le (hy.trans_lt ENNReal.ofReal_lt_top).ne hxy hy).trans_eq
(tsub_add_cancel_of_le <| le_self_add.trans (lt_tsub_iff_left.1 hxy).le))
