leftInverse

Mathlib.Geometry.Manifold.IsManifold.Basic

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

English

There exists a LeftInverse for I.symm and I, i.e., I.symm acts as a left inverse of I.

Русский

Существуют левая обратная функция для I.symm и I, то есть I.symm выступает как левая обратная функция к I.

LaTeX

$$$ \\text{LeftInverse } I.symm I $$$

Lean4

protected theorem leftInverse : LeftInverse I.symm I :=
  I.left_inv

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

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

Разделы

Аффилиация

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