isOpen_extend_target — Mathlib

English

The extended target equals the image of f.target under I, i.e., (f.extend I).target = I.image f.target.

Русский

Расширенная цель равна образу целевой диаграммы f.target под I.

LaTeX

$$(f.extend I).target = I.image' f.target$$

Lean4

theorem isOpen_extend_target [I.Boundaryless] : IsOpen (f.extend I).target :=
  by
  rw [extend_target, I.range_eq_univ, inter_univ]
  exact I.continuous_symm.isOpen_preimage _ f.open_target

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