comap — Mathlib

English

Pullback of a covering along a continuous map yields a covering in the domain with the same index type.

Русский

Вытяжка покрытия по непрерывному отображению даёт покрытие в области области с тем же индексом.

LaTeX

$$comap (hv : IsOpenCover v) (f : ContinuousMap X Y) : IsOpenCover (fun k => (v k).comap f)$$

Lean4

/-- Pullback of a covering of `Y` by a continuous map `X → Y`, giving a covering of `X` with the
same index type. -/
theorem comap (hv : IsOpenCover v) (f : C(X, Y)) : IsOpenCover fun k ↦ (v k).comap f := by
  simp [IsOpenCover, ← preimage_iUnion, hv.iSup_set_eq_univ]

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