isOpen_extend_preimage — Mathlib

English

The extended target is eventually equal to the range I along neighborhoods of the extended image.

Русский

Расширенная цель в пределе равна диапазону I вдоль окрестностей образа.

LaTeX

$$$ (f.extend I).target =^\\mathrm{f}_{\\mathcal{N}(f.extend I y)} \\operatorname{range}(I). $$$

Lean4

theorem isOpen_extend_preimage {s : Set E} (hs : IsOpen s) : IsOpen (f.source ∩ f.extend I ⁻¹' s) := by
  rw [← extend_source f (I := I)]; exact isOpen_extend_preimage' f hs

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