grothendieckTopology_monotone — Mathlib

English

If P ≤ Q as morphism properties, then grothendieckTopology P ≤ grothendieckTopology Q; monotonicity of the Grothendieck topology with respect to the base property.

Русский

Если P ≤ Q как свойства морфизмов, тогда grothendieckTopology P ≤ grothendieckTopology Q; монотонность топологии Гротенддик по отношению к базовому свойству.

LaTeX

$$$P \\leq Q \\Rightarrow grothendieckTopology P \\leq grothendieckTopology Q$$$

Lean4

theorem grothendieckTopology_monotone (hPQ : P ≤ Q) : grothendieckTopology P ≤ grothendieckTopology Q :=
  (Pretopology.gi Scheme.{u}).gc.monotone_l (pretopology_monotone hPQ)

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