instIsContinuousOpensCarrierMapGrothendieckTopology

English

The induced Opens.map f is continuous between Grothendieck topologies on X and Y.

Русский

Индуцированный Opens.map f непрерывен между топологиями Grothendieck на X и Y.

LaTeX

$$$\text{IsContinuous}((Opens.map\, f),\; Opens.grothendieckTopology\; Y,\; Opens.grothendieckTopology\; X)$$$

Lean4

instance : (Opens.map f).IsContinuous (Opens.grothendieckTopology Y) (Opens.grothendieckTopology X) :=
  by
  apply Functor.isContinuous_of_coverPreserving
  · exact compatiblePreserving_opens_map f
  · exact coverPreserving_opens_map f

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