pullback — Mathlib

English

If f: X → Y is a separated map, then the second projection from the pullback of f is also separated.

Русский

Если f: X → Y — разделяющее отображение, тогда в вытащенном по f произведении проекция вторая также разделяющая.

LaTeX

$$$\mathrm{IsSeparatedMap}(f) \rightarrow \mathrm{IsSeparatedMap}(\mathrm{snd}\,X\,Y\,A\,f\,g)$$$

Lean4

theorem pullback {f : X → Y} (sep : IsSeparatedMap f) (g : A → Y) : IsSeparatedMap (@snd X Y A f g) :=
  by
  rw [isSeparatedMap_iff_isClosed_diagonal] at sep ⊢
  rw [← preimage_map_fst_pullbackDiagonal]
  refine sep.preimage (Continuous.mapPullback ?_ ?_) <;>
    apply_rules [continuous_fst, continuous_subtype_val, Continuous.comp]

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