left_inv — Mathlib

English

The right inverse property holds: applying e.symm after e to any element x of the source yields x.

Русский

Правое обратное свойство: применение e.symm после e к любому элементу исходной области даёт исходный элемент.

LaTeX

$$$\forall x\in e. source,\ e( e.symm(x) ) = x$$$

Lean4

@[simp, mfld_simps]
theorem left_inv {x : α} (h : x ∈ e.source) : e.symm (e x) = x :=
  e.left_inv' h

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