map_continuousOn — Mathlib

English

If γ is a path in F from x to y and f is continuous on F, then the composition f ∘ γ is a path in f(F) from f(x) to f(y).

Русский

Если γ — путь в F от x к y, а f непрерывна на F, то композиция f ∘ γ — путь в f(F) от f(x) к f(y).

LaTeX

$$JoinedIn F x y → (∀ f, ContinuousOn f F → JoinedIn (f''F) (f x) (f y))$$

Lean4

theorem map_continuousOn (h : JoinedIn F x y) {f : X → Y} (hf : ContinuousOn f F) : JoinedIn (f '' F) (f x) (f y) :=
  let ⟨γ, hγ⟩ := h
  ⟨γ.map' <| hf.mono (range_subset_iff.mpr hγ), fun t ↦ mem_image_of_mem _ (hγ t)⟩

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