perm_inv

Mathlib.GroupTheory.Perm.Basic

URI: https://scilib.ai/kg/mathlib#Set.BijOn.perm_inv

English

If f is a bijection on a set s, then its inverse f^{-1} also gives a bijection on s; equivalently, the inverse map is a bijection on s.

Русский

Если f биекция на s, то и её обратная карта f^{-1} задаёт биекцию на s.

LaTeX

$$$\\text{BijOn } f\, s\, s \\Rightarrow \\text{BijOn } (f^{-1})\, s\, s$$$

Lean4

theorem perm_inv (hf : BijOn f s s) : BijOn (↑(f⁻¹)) s s :=
  hf.symm f.invOn

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

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

Разделы

Аффилиация

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