Theorems · Theorem · algebraic geometry

AlgebraicGeometry.reduce_to_affine_nbhd

∀ (P : (X : AlgebraicGeometry.Scheme) → ↥X → Prop),
  (∀ (R : CommRingCat) (x : ↥(AlgebraicGeometry.Spec R)), P (AlgebraicGeometry.Spec R) x) →
    (∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (x : ↥X), P X x → P Y (f x)) →
      ∀ (X : AlgebraicGeometry.Scheme) (x : ↥X), P X x

Defined in

Mathlib.AlgebraicGeometry.Properties

Cited by

0 results in Mathlib

Foundations

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