apply_invFun_apply

Mathlib.Logic.Function.Basic

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

Lean4

theorem apply_invFun_apply {α β : Type*} {f : α → β} {a : α} : f (@invFun _ _ ⟨a⟩ f (f a)) = f a :=
  @invFun_eq _ _ ⟨a⟩ _ _ ⟨_, rfl⟩

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

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

Разделы

Аффилиация

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