interior_extend_target_subset_interior_range

English

The interior of the extended target is contained in the interior of the range of I.

Русский

Внутренняя часть целевой области расширенного чартa содержится внутри внутренности диапазона I.

LaTeX

$$$ \\operatorname{Int}((f^{\\mathrm{extend}}_I).\\mathrm{target}) \\subseteq \\operatorname{Int}(\\operatorname{range}(I)). $$$

Lean4

theorem interior_extend_target_subset_interior_range : interior (f.extend I).target ⊆ interior (range I) :=
  by
  rw [f.extend_target, interior_inter, (f.open_target.preimage I.continuous_symm).interior_eq]
  exact inter_subset_right

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