isConnected_preimage

Mathlib.Topology.Homeomorph.Lemmas

URI: https://scilib.ai/kg/mathlib#Homeomorph.isConnected_preimage

English

If h is a homeomorphism, IsPreconnected(h^{-1}(s)) holds iff IsPreconnected(s) for s ⊆ Y.

Русский

Если h — гомеоморфизм, то IsPreconnected(h^{-1}(s)) эквивалентно IsPreconnected(s) для s ⊆ Y.

LaTeX

$$$IsPreconnected(h^{-1}(s)) \\iff IsPreconnected(s)$$$

Lean4

@[simp]
theorem isConnected_preimage {s : Set Y} (h : X ≃ₜ Y) : IsConnected (h ⁻¹' s) ↔ IsConnected s := by
  rw [← image_symm, isConnected_image]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru