invFun_comp

Mathlib.Logic.Function.Basic

URI: https://scilib.ai/kg/mathlib#Function.invFun_comp

English

If f is injective, then invFun f ∘ f = id.

Русский

Если f инъективна, то invFun f ∘ f = id.

LaTeX

$$$ \text{Injective}(f) \rightarrow \mathrm{invFun}(f) \circ f = \mathrm{id} $$$

Lean4

theorem invFun_comp (hf : Injective f) : invFun f ∘ f = id :=
  funext <| leftInverse_invFun hf

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

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

Разделы

Аффилиация

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