eq_isFinite_inf_mono — Mathlib

English

IsClosedImmersion equals the infimum of IsFinite and mono properties.

Русский

IsClosedImmersion равен минимуму свойств IsFinite и моно.

LaTeX

$$$\mathrm{IsClosedImmersion} = \inf\big(\mathrm{IsFinite}, \mathrm{monomorphisms\ Scheme}\big).$$$

Lean4

theorem _root_.AlgebraicGeometry.IsClosedImmersion.eq_isFinite_inf_mono :
    @IsClosedImmersion = (@IsFinite ⊓ monomorphisms Scheme : MorphismProperty _) := by ext;
  exact IsClosedImmersion.iff_isFinite_and_mono _

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