English
Let f: X → Y be an open map between topological spaces. Then for every open U ⊆ X and every open cover {U_i} of U, the family {f(U_i)} is a cover of f(U) in the Grothendieck topology on Opens(Y).
Русский
Пусть f: X → Y — открытое отображение. Тогда для любого открытого U ⊆ X и любого открытого покрытия {U_i} U вершины, семейство {f(U_i)} покрывает f(U) в GrothendieckTopology( Opens(Y) ).
LaTeX
$$$$ \operatorname{CoverPreserving}\bigl( \operatorname{Opens.grothendieckTopology}(X), \operatorname{Opens.grothendieckTopology}(Y), \operatorname{Opens.map}(f) \bigr). $$$$
Lean4
theorem coverPreserving (hf : IsOpenMap f) :
CoverPreserving (Opens.grothendieckTopology X) (Opens.grothendieckTopology Y) hf.functor :=
by
constructor
rintro U S hU _ ⟨x, hx, rfl⟩
obtain ⟨V, i, hV, hxV⟩ := hU x hx
exact ⟨_, hf.functor.map i, ⟨_, i, 𝟙 _, hV, rfl⟩, Set.mem_image_of_mem f hxV⟩
