isOpen_image_iff_of_subset_source

English

IsOpen of the image equals IsOpen of the source when the subset is contained in the source.

Русский

Открытость образа равна открытости источника при условии, что подмножество содержится в источнике.

LaTeX

$$$IsOpen (e '' s) \\Leftrightarrow IsOpen s$ при $s \\subseteq e.source$$$

Lean4

theorem isOpen_image_iff_of_subset_source {s : Set X} (hs : s ⊆ e.source) : IsOpen (e '' s) ↔ IsOpen s := by
  rw [← e.symm.isOpen_symm_image_iff_of_subset_target hs, e.symm_symm]

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