range_eq

Mathlib.Order.Hom.Set

URI: https://scilib.ai/kg/mathlib#OrderIso.range_eq

English

For an order isomorphism e: α ≃o β, the image of α is all of β; i.e., e is surjective.

Русский

Для изоморфизма порядка e: α ≃o β образ α равен β; то есть e сюръективен.

LaTeX

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

Lean4

theorem range_eq (e : α ≃o β) : Set.range e = Set.univ :=
  e.surjective.range_eq

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

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

Разделы

Аффилиация

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