rightInvOn

Mathlib.Geometry.Manifold.IsManifold.Basic

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

English

On the range of I, I.symm is a right inverse of I; i.e., for any y in range(I), I.symm(I(y)) = y.

Русский

На диапазоне I I.symm является правой обратной к I; то есть для любого y из range(I) верно I.symm(I(y)) = y.

LaTeX

$$$ \\forall y \\in \\mathrm{range}(I),\\; I.symm(I(y)) = y $$$

Lean4

protected theorem rightInvOn : RightInvOn I.symm I (range I) :=
  I.leftInverse.rightInvOn_range

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

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

Разделы

Аффилиация

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