ofLeftInverse'_apply — Mathlib

English

The forward map of the isomorphism produced by range restriction matches the original morphism f.

Русский

Поскольку полученный изоморфизм строится через ограничение диапазона, его переходная карта совпадает с исходным отображением f.

LaTeX

$$$(\mathrm{ofLeftInverse'}(h))(x) = f(x).$$$

Lean4

@[simp]
theorem ofLeftInverse'_apply {g : B → A} {f : F} (h : Function.LeftInverse g f) (x : A) : ofLeftInverse' h x = f x :=
  rfl

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