mem_interior_extend_target — Mathlib

English

If y lies in the target, the extension is continuous at the corresponding point and the inverse is continuous there as well.

Русский

Если y ∈ target, расширение непрерывно в соответствующей точке и обратное отображение тоже непрерывно там.

LaTeX

$$$ y \\in f.target \\Rightarrow \\text{ContinuousAt}(f^{\\mathrm{extend}}_I)^{-1}(y) \\text{ and } \\text{ContinuousAt}(f^{\\mathrm{extend}}_I)(y). $$$

Lean4

/-- If `y ∈ f.target` and `I y ∈ interior (range I)`,
then `I y` is an interior point of `(I ∘ f).target`. -/
theorem mem_interior_extend_target {y : H} (hy : y ∈ f.target) (hy' : I y ∈ interior (range I)) :
    I y ∈ interior (f.extend I).target :=
  by
  rw [f.extend_target, interior_inter, (f.open_target.preimage I.continuous_symm).interior_eq, mem_inter_iff,
    mem_preimage]
  exact ⟨mem_of_eq_of_mem (I.left_inv (y)) hy, hy'⟩

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