isQuasiSeparated_iff — Mathlib

English

For an open embedding f, a subset s is quasi-separated iff its image f''s is quasi-separated.

Русский

Для открытого вложения f подмножество s квазиразделимо тогда и только тогда, когда образ f''s квазиразделим.

LaTeX

$$IsOpenEmbedding(f) \\Rightarrow (IsQuasiSeparated(s) \\iff IsQuasiSeparated(f''s))$$

Lean4

theorem isQuasiSeparated_iff (h : IsOpenEmbedding f) {s : Set α} : IsQuasiSeparated s ↔ IsQuasiSeparated (f '' s) :=
  by
  refine ⟨fun hs => hs.image_of_isEmbedding h.isEmbedding, ?_⟩
  intro H U V hU hU' hU'' hV hV' hV''
  rw [h.isEmbedding.isCompact_iff, Set.image_inter h.injective]
  exact
    H (f '' U) (f '' V) (image_mono hU) (h.isOpenMap _ hU') (hU''.image h.continuous) (image_mono hV)
      (h.isOpenMap _ hV') (hV''.image h.continuous)

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