English
Let h be a homeomorphism X ≃ Y. Then h maps the connected component of x in s to the connected component of h(x) in h[s], i.e., h[connectedComponentIn(s, x)] = connectedComponentIn(h[s], h(x)) whenever x ∈ s.
Русский
Пусть h — гомеоморфизм X ≃ Y. Тогда образ компонентной связности x в s равен компоненте связности h(x) в h[s], т.е. h[connectedComponentIn(s, x)] = connectedComponentIn(h[s], h(x)) при условии x ∈ s.
LaTeX
$$$h''(\\\\text{connectedComponentIn}(s, x)) = \\\\text{connectedComponentIn}(h''s, h(x))$ при \\(x \\in s\\)$$
Lean4
theorem image_connectedComponentIn {s : Set X} (h : X ≃ₜ Y) {x : X} (hx : x ∈ s) :
h '' connectedComponentIn s x = connectedComponentIn (h '' s) (h x) :=
by
refine (h.continuous.image_connectedComponentIn_subset hx).antisymm ?_
have := h.symm.continuous.image_connectedComponentIn_subset (mem_image_of_mem h hx)
rwa [image_subset_iff, h.preimage_symm, h.image_symm, h.preimage_image, h.symm_apply_apply] at this
