isOpen_image_symm_of_subset_target

English

The inverse image of an open subset of the target under e.symm is open.

Русский

Обратное отображение открыто в целевой части для подмножества.

LaTeX

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

Lean4

/-- The inverse of an open partial homeomorphism `e` is an open map on `e.target`. -/
theorem isOpen_image_symm_of_subset_target {t : Set Y} (ht : IsOpen t) (hte : t ⊆ e.target) : IsOpen (e.symm '' t) :=
  isOpen_image_of_subset_source e.symm ht (e.symm_source ▸ hte)

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