instOfIsFinite

Mathlib.AlgebraicGeometry.Morphisms.Proper

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsProper.instOfIsFinite

English

If a morphism f is finite, then f is proper.

Русский

Если морфизм f конечен, то он является корректным (proper).

LaTeX

$$$[\text{IsFinite } f] \Rightarrow \text{IsProper}(f)$$$

Lean4

instance (priority := 900) [IsFinite f] : IsProper f where

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

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

Разделы

Аффилиация

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