isTotallyDisconnected_of_image — Mathlib

English

If f is continuous on s and injective, then IsTotallyDisconnected (image f s) implies IsTotallyDisconnected s.

Русский

Если f непрерывно на s и инъективно, то TD образа f(s) влечет TD самого s.

LaTeX

$$IsTotallyDisconnected (Set.image f s) ⇔ IsTotallyDisconnected s$$

Lean4

theorem isTotallyDisconnected_of_image [TopologicalSpace β] {f : α → β} (hf : ContinuousOn f s) (hf' : Injective f)
    (h : IsTotallyDisconnected (f '' s)) : IsTotallyDisconnected s := fun _t hts ht _x x_in _y y_in =>
  hf' <| h _ (image_mono hts) (ht.image f <| hf.mono hts) (mem_image_of_mem f x_in) (mem_image_of_mem f y_in)

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