English
If f is an open embedding, then the forward Open-set map functor induced by f is continuous between the Grothendieck topologies on X and Y; in particular, it is continuous with respect to covers and compatible families.
Русский
Если f — открытое вложение, то соответствующий функтор перехода между множествами открытых множеств, индуцированный f, непрерывен относительноGrothendieckTopology(X) иGrothendieckTopology(Y).
LaTeX
$$$$ \\mathrm{IsContinuous}\\bigl( (\\mathrm{Opens.map}\\ f) : \\mathrm{Opens}(X) \\to \\mathrm{Opens}(Y) \\bigr) \\quad\\text{with respect to } \\operatorname{Opens.grothendieckTopology}(X), \\operatorname{Opens.grothendieckTopology}(Y). $$$$
Lean4
theorem functor_isContinuous (h : IsOpenEmbedding f) :
h.isOpenMap.functor.IsContinuous (Opens.grothendieckTopology X) (Opens.grothendieckTopology Y) :=
by
apply Functor.isContinuous_of_coverPreserving
· exact h.compatiblePreserving
· exact h.isOpenMap.coverPreserving
