∀ {P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : P.IsMultiplicative] [inst_2 : P.RespectsIso]
  [inst_3 : Q.IsStableUnderComposition] [inst_4 : Q.IsStableUnderBaseChange] [inst_5 : Q.HasOfPostcompProperty Q]
  (hPQ : P ≤ Q), S.smallGrothendieckTopologyOfLE hPQ = (AlgebraicGeometry.Scheme.smallPretopology P Q).toGrothendieck