infEdist_le_infEdist_thickening_add

English

Let K be compact, f: α→β, U open in β, and K mapped into U with f continuous at points of K. Then there exists ε>0 and V∈nhdsˢK such that thickening ε of f''V sits inside U.

Русский

Пусть K компактно, f: α→β, U открыто в β, f(K)⊆U и f непрерывна на K. Тогда существует ε>0 и V∈nhdsˢK such that thickening_{ε}(f''V) ⊆ U.

LaTeX

$$$\exists ε>0,\exists V∈𝓝^{s} K:\;\operatorname{thickening}_{ε}(f''V) ⊆ U$$$

Lean4

/-- For the equality, see `infEdist_thickening`. -/
theorem infEdist_le_infEdist_thickening_add : infEdist x s ≤ infEdist x (thickening δ s) + ENNReal.ofReal δ :=
  infEdist_le_infEdist_cthickening_add.trans <| add_le_add_right (infEdist_anti <| thickening_subset_cthickening _ _) _

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