Theorems · Theorem · algebraic geometry

AlgebraicGeometry.universally_isZariskiLocalAtTarget

∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme),
  (∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
      TopologicalSpace.IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f) →
    AlgebraicGeometry.IsZariskiLocalAtTarget P.universally

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Constructors

Cited by

0 results in Mathlib

Foundations

Depth 149 from the axioms · uses propext, Classical.choice, Quot.sound