inducedTopology_coverPreserving — Mathlib

English

The induced topology is cover-preserving with respect to K and G, meaning that pushing forward coverings along G preserves covering sieves in the target topology K.

Русский

Вводимая топология сохраняет покрытия: отображение образов покрывающих сита через G сохраняет покрытия в топологии K на D.

LaTeX

$$$\\mathrm{CoverPreserving}\\big( G.\\mathrm{inducedTopology } K\\big)\\; K\\; G$$$

Lean4

/-- `G` is cover-preserving w.r.t. the induced topology. -/
theorem inducedTopology_coverPreserving : CoverPreserving (G.inducedTopology K) K G :=
  ⟨@fun _ _ hS => hS⟩

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