eq_inf — Mathlib

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 _

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