bijective_id

Mathlib.Logic.Function.Defs

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

English

The identity map is bijective.

Русский

Тождественный отображатель биективен.

LaTeX

$$$ \text{Bijective}(id) $$$

Lean4

theorem bijective_id : Bijective (@id α) :=
  ⟨injective_id, surjective_id⟩

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

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

Разделы

Аффилиация

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