swap_bijective

Mathlib.Data.Prod.Basic

URI: https://scilib.ai/kg/mathlib#Prod.swap_bijective

English

Swap is bijective.

Русский

Swap является биективным.

LaTeX

$$$\\\\operatorname{Bijective}(\\\\operatorname{swap}).$$$

Lean4

theorem swap_bijective : Function.Bijective (@swap α β) :=
  ⟨swap_injective, swap_surjective⟩

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

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

Разделы

Аффилиация

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