right_inv — Mathlib

English

Let I be a model with corners. Then for every y in the image of I, applying the inverse map I^{-1} and then I returns y; i.e., I(I^{-1}(y)) = y for all y with y ∈ range(I).

Русский

Пусть I — модель с углами. Тогда для каждого y из образа I выполнено I(I^{-1}(y)) = y; то есть при применении обратной функции I^{-1} к y и последующем применении I получаем y, если y лежит в range(I).

LaTeX

$$$\\forall y \\in \\operatorname{range}(I),\\quad I(I^{-1}(y)) = y$$$

Lean4

@[simp, mfld_simps]
protected theorem right_inv {x : E} (hx : x ∈ range I) : I (I.symm x) = x :=
  I.rightInvOn hx

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