isOpen_extend_source

Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

URI: https://scilib.ai/kg/mathlib#OpenPartialHomeomorph.isOpen_extend_source

English

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

Русский

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

LaTeX

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

Lean4

theorem isOpen_extend_source : IsOpen (f.extend I).source :=
  by
  rw [extend_source]
  exact f.open_source

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru