surjective

Mathlib.Logic.Equiv.Defs

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

English

For any e: α ≃ β, the forward map e is surjective.

Русский

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

LaTeX

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

Lean4

protected theorem surjective (e : α ≃ β) : Surjective e :=
  EquivLike.surjective e

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

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

Разделы

Аффилиация

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