isPathConnected_iff — Mathlib

English

If f is an inducing map, F is path-connected iff f''F is path-connected.

Русский

Если f — индуцирующая отображение, то F связно по траекториям тогда и только тогда, когда f(F) связано по траекториям.

LaTeX

$$$$\text{IsInducing}(f) \Rightarrow (\IsPathConnected(F) \iff \IsPathConnected(f''F)).$$$$

Lean4

/-- If `f : X → Y` is an inducing map, `f(F)` is path-connected iff `F` is. -/
nonrec theorem isPathConnected_iff {f : X → Y} (hf : IsInducing f) : IsPathConnected F ↔ IsPathConnected (f '' F) :=
  by
  simp only [IsPathConnected, forall_mem_image, exists_mem_image]
  refine exists_congr fun x ↦ and_congr_right fun hx ↦ forall₂_congr fun y hy ↦ ?_
  rw [hf.joinedIn_image hx hy]

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