extend_source

Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

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

English

The source of the extended chart equals the source of f, i.e., (f.extend I).source = f.source.

Русский

Источник расширенной диаграммы совпадает с источником f.

LaTeX

$$extend_source : (f.extend I).source = f.source$$

Lean4

theorem extend_source : (f.extend I).source = f.source := by
  rw [extend, PartialEquiv.trans_source, I.source_eq, preimage_univ, inter_univ]

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

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

Разделы

Аффилиация

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