isOpen_image_of_subset_source — Mathlib

English

The image of an open subset of the source is open.

Русский

Образ открытого подмножества источника открыт.

LaTeX

$$$IsOpen (e '' s)\\; \\text{ при } IsOpen s \\text{ и } s \\subseteq e.source$$$

Lean4

/-- An open partial homeomorphism is an open map on its source:
  the image of an open subset of the source is open. -/
theorem isOpen_image_of_subset_source {s : Set X} (hs : IsOpen s) (hse : s ⊆ e.source) : IsOpen (e '' s) :=
  by
  rw [(image_eq_target_inter_inv_preimage (e := e) hse)]
  exact e.continuousOn_invFun.isOpen_inter_preimage e.open_target hs

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