image_connectedComponent — Mathlib

English

For a quotient map f with connected fibers, the image of the connected component of a is the connected component of f(a).

Русский

Для тождественного отображения f с связными волокнами образ связной компоненты a равен связной компоненте f(a).

LaTeX

$$$f''\operatorname{connectedComponent}(a) = \operatorname{connectedComponent}(f(a))$$$

Lean4

theorem image_connectedComponent {f : α → β} (hf : IsQuotientMap f) (h_fibers : ∀ y : β, IsConnected (f ⁻¹' { y }))
    (a : α) : f '' connectedComponent a = connectedComponent (f a) := by
  rw [← hf.preimage_connectedComponent h_fibers, image_preimage_eq _ hf.surjective]

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