iff — Mathlib

English

HasAffineProperty P Q is equivalent to IsZariskiLocalAtTarget P and Q = of P.

Русский

HasAffineProperty P Q эквивалентно IsZariskiLocalAtTarget P и Q = of P.

LaTeX

$$$HasAffineProperty P Q \iff(IsZariskiLocalAtTarget P \land Q = of P)$$$

Lean4

protected theorem iff {P : MorphismProperty Scheme} {Q : AffineTargetMorphismProperty} :
    HasAffineProperty P Q ↔ IsZariskiLocalAtTarget P ∧ Q = of P :=
  ⟨fun _ ↦ ⟨inferInstance, ext fun _ _ _ ↦ iff_of_isAffine.symm⟩, fun ⟨_, e⟩ ↦ e ▸ of_isZariskiLocalAtTarget P⟩

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