left_inv

Mathlib.Geometry.Manifold.IsManifold.Basic

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

English

The left inverse of I.symm and I is defined; for all x in H, I.symm(I(x)) = x.

Русский

Левая обратная функция для I.symm и I задана; для всех x в H выполняется I.symm(I(x)) = x.

LaTeX

$$$ \\forall x:\\, I.symm(I(x)) = x $$$

Lean4

@[simp, mfld_simps]
protected theorem left_inv (x : H) : I.symm (I x) = x := by refine I.left_inv' ?_; simp

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

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

Разделы

Аффилиация

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