preimage_of_isClosedMap — Mathlib

English

Under the assumptions of openness and disjointness, if s ⊆ u ∪ v and s ∩ u is nonempty, then s ⊆ u.

Русский

При условии открытости и взаимной непересекаемости, если s ⊆ u ∪ v и s ∩ u ≠ ∅, то s ⊆ u.

LaTeX

$$$\\text{IsOpen}(u) \\land \\text{IsOpen}(v) \\land \\text{Disjoint}(u,v) \\land s \\subseteq u \\cup v \\land (s \\cap u) \\neq \\varnothing \\Rightarrow s \\subseteq u$$$

Lean4

theorem preimage_of_isClosedMap [TopologicalSpace β] {s : Set β} (hs : IsConnected s) {f : α → β}
    (hinj : Function.Injective f) (hf : IsClosedMap f) (hsf : s ⊆ range f) : IsConnected (f ⁻¹' s) :=
  ⟨hs.nonempty.preimage' hsf, hs.isPreconnected.preimage_of_isClosedMap hinj hf hsf⟩

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