target_eq

Mathlib.Geometry.Manifold.IsManifold.Basic

URI: https://scilib.ai/kg/mathlib#ModelWithCorners.target_eq

English

The target of I equals the range of the coordinate map I.toFun'.

Русский

Цель I равна диапазону отображения координат I.toFun'.

LaTeX

$$$ I.target = \\mathrm{range}(I.toFun') $$$

Lean4

@[simp, mfld_simps]
theorem target_eq : I.target = range (I : H → E) :=
  by
  rw [← image_univ, ← I.source_eq]
  exact I.image_source_eq_target.symm

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

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

Разделы

Аффилиация

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