isTotallyDisconnected — Mathlib

English

If f is an embedding, then IsTotallyDisconnected (Set.image f s) ⇔ IsTotallyDisconnected s.

Русский

Если f — вложение (embedding), то IsTotallyDisconnected (образ f(s)) эквивалентно IsTotallyDisconnected s.

LaTeX

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

Lean4

theorem isTotallyDisconnected [TopologicalSpace β] {f : α → β} {s : Set α} (hf : IsEmbedding f)
    (h : IsTotallyDisconnected (f '' s)) : IsTotallyDisconnected s :=
  isTotallyDisconnected_of_image hf.continuous.continuousOn hf.injective h

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