comp_surjInv

Mathlib.Logic.Function.Basic

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

English

For any surjective f, f ∘ f.surjInv hf = id.

Русский

Для сюръективной f выполняется f ∘ surjInv hf = id.

LaTeX

$$$ \text{Surjective}(f) \rightarrow f \circ f.surjInv(hf) = \mathrm{id}$$$

Lean4

@[simp]
theorem comp_surjInv (hf : f.Surjective) : f ∘ f.surjInv hf = id :=
  funext (Function.surjInv_eq _)

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

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

Разделы

Аффилиация

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