English
The finite morphism property equals the infimum of integral morphism and locally finite type properties in the lattice of morphism properties.
Русский
Свойство конечности морфизма равно наименьшему из двух свойств: интегральности и локального конечного типа, в соответствующей решетке свойств морфизмов.
LaTeX
$$$\mathrm{IsFinite} = \inf\big(\mathrm{IsIntegralHom}, \mathrm{LocallyOfFiniteType}\big).$$$
Lean4
theorem eq_inf : @IsFinite = (@IsIntegralHom ⊓ @LocallyOfFiniteType : MorphismProperty Scheme) := by ext;
exact IsFinite.iff_isIntegralHom_and_locallyOfFiniteType _