range_eq_univ

Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

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

English

If f: X → Y is surjective, then the range of the underlying map f_base is the whole underlying space |Y|.

Русский

Если f сюръективен, то образ базового отображения f_base равно всему множеству |Y|.

LaTeX

$$$\operatorname{range}(f_{\mathrm{base}}) = |Y|$$$

Lean4

@[simp]
theorem range_eq_univ [Surjective f] : Set.range f.base = Set.univ := by simpa [Set.range_eq_univ] using f.surjective

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

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

Разделы

Аффилиация

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