isTotallyDisconnected_image — Mathlib

English

The same as above: IsTotallyDisconnected (Set.image f s) ↔ IsTotallyDisconnected s for an embedding f.

Русский

То же самое: IsTotallyDisconnected (образ f(s)) ↔ IsTotallyDisconnected s для вложения f.

LaTeX

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

Lean4

theorem isTotallyDisconnected_image [TopologicalSpace β] {f : α → β} {s : Set α} (hf : IsEmbedding f) :
    IsTotallyDisconnected (f '' s) ↔ IsTotallyDisconnected s :=
  by
  refine ⟨hf.isTotallyDisconnected, fun hs u hus hu ↦ ?_⟩
  obtain ⟨v, hvs, rfl⟩ : ∃ v, v ⊆ s ∧ f '' v = u :=
    ⟨f ⁻¹' u ∩ s, inter_subset_right, by rwa [image_preimage_inter, inter_eq_left]⟩
  rw [hf.isInducing.isPreconnected_image] at hu
  exact (hs v hvs hu).image _

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