range_eq_univ

Mathlib.Logic.Equiv.Set

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

English

For an equivalence e, the underlying function e: α → β is surjective, hence its range is univ.

Русский

Для эквивалентности e соответствующая функция e: α → β сюръективна, следовательно её образ равен univ.

LaTeX

$$$\operatorname{range}(e) = \mathrm{univ}.$$$

Lean4

theorem range_eq_univ {α : Type*} {β : Type*} (e : α ≃ β) : range e = univ :=
  EquivLike.range_eq_univ e

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

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

Разделы

Аффилиация

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