bijective

Mathlib.Logic.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.bijective

English

For any e: α ≃ β, the forward function e is bijective.

Русский

Для любой e: α ≃ β отображение e является биективным.

LaTeX

$$$\forall e:\alpha \simeq \beta,\ \text{Bijective}(e.toFun)$$$

Lean4

protected theorem bijective (e : α ≃ β) : Bijective e :=
  EquivLike.bijective e

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

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

Разделы

Аффилиация

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