coverPreserving_opens_map — Mathlib

English

The map on opens preserves coverings: a cover of an open set in Y pulls back to a cover in X via Opens.map f.

Русский

Покрытие открытого множества в Y переносится в покрытие в X через Opens.map f.

LaTeX

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

Lean4

theorem coverPreserving_opens_map :
    CoverPreserving (Opens.grothendieckTopology Y) (Opens.grothendieckTopology X) (Opens.map f) :=
  by
  constructor
  intro U S hS x hx
  obtain ⟨V, i, hi, hxV⟩ := hS (f x) hx
  exact ⟨_, (Opens.map f).map i, ⟨_, _, 𝟙 _, hi, Subsingleton.elim _ _⟩, hxV⟩

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