toProperty_apply — Mathlib

English

For any P in AffineTargetMorphismProperty and a morphism f: X → Y with Y affine, the associated property P.toProperty matches P.

Русский

Для P в AffineTargetMorphismProperty и морфизма f: X → Y с Y аффинный, соответствующее свойство P.toProperty совпадает с P.

LaTeX

$$$\forall P : \mathrm{AffineTargetMorphismProperty}, \forall X Y : \mathrm{Scheme}, \forall f : X \to Y \, [\mathrm IsAffine Y],\ P^{\mathrm{toProperty}}(f) \iff P(f).$$$

Lean4

theorem toProperty_apply (P : AffineTargetMorphismProperty) {X Y : Scheme} (f : X ⟶ Y) [i : IsAffine Y] :
    P.toProperty f ↔ P f := by delta AffineTargetMorphismProperty.toProperty; simp [*]

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