image — Mathlib

English

If f is continuous on all of X and F is path-connected, then f(F) is path-connected.

Русский

Если f непрерывна на всей X и F связно по траекториям, то образ f(F) связан по траекториям.

LaTeX

$$$$\IsPathConnected(F) \rightarrow \IsPathConnected(f(F)) \text{ for continuous } f.$$$$

Lean4

/-- If `f` is continuous and `F` is path-connected, so is `f(F)`. -/
theorem image (hF : IsPathConnected F) {f : X → Y} (hf : Continuous f) : IsPathConnected (f '' F) :=
  hF.image' hf.continuousOn

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