English
Let f: α → β be a quotient map. Suppose that for every y ∈ β the fiber f^{-1}({y}) is connected. Then for every a ∈ α, f^{-1}(connectedComponent(f(a))) = connectedComponent(a).
Русский
Пусть f: α → β — факторное отображение. Предположим, что для каждого y ∈ β множество f^{-1}({y}) связано. Тогда для любого a ∈ α выполняется f^{-1}(connectedComponent(f(a))) = connectedComponent(a).
LaTeX
$$$f^{-1}(\operatorname{connectedComponent}(f(a))) = \operatorname{connectedComponent}(a)$$$
Lean4
theorem preimage_connectedComponent (hf : IsQuotientMap f) (h_fibers : ∀ y : β, IsConnected (f ⁻¹' { y })) (a : α) :
f ⁻¹' connectedComponent (f a) = connectedComponent a :=
((preimage_connectedComponent_connected h_fibers (fun _ => hf.isClosed_preimage.symm) _).subset_connectedComponent
mem_connectedComponent).antisymm
(hf.continuous.mapsTo_connectedComponent a)
