Theorems · Theorem · algebraic geometry

AlgebraicGeometry.affineLocally_le

∀ {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, P f → Q f) →
    (AlgebraicGeometry.affineLocally fun {R S} [CommRing R] [CommRing S] => P) ≤
      AlgebraicGeometry.affineLocally fun {R S} [CommRing R] [CommRing S] => Q

Defined in

Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Cited by

0 results in Mathlib

Foundations

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