isOpen_symm_image_iff_of_subset_target

English

IsOpen of the inverse image equals IsOpen of the target, provided subset condition.

Русский

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

LaTeX

$$$IsOpen (e.symm '' t) \\Leftrightarrow IsOpen t$ при $t \\subseteq e.target$$$

Lean4

theorem isOpen_symm_image_iff_of_subset_target {t : Set Y} (hs : t ⊆ e.target) : IsOpen (e.symm '' t) ↔ IsOpen t :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ e.symm.isOpen_image_of_subset_source h hs⟩
  have hs' : e.symm '' t ⊆ e.source :=
    by
    rw [e.symm_image_eq_source_inter_preimage hs]
    apply Set.inter_subset_left
  rw [← e.image_symm_image_of_subset_target hs]
  exact e.isOpen_image_of_subset_source h hs'

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