comp_right — Mathlib

English

If f: X → Y is separated, and g: A → X is continuous and injective, then f ∘ g is separated.

Русский

Если f разделяющее отображение, а g: A → X непрерывен и инъективен, то f ∘ g разделяющее.

LaTeX

$$$\mathrm{IsSeparatedMap}(f) \rightarrow (\mathrm{Continuous}(g) \land g\text{ injective}) \rightarrow \mathrm{IsSeparatedMap}(f\circ g)$$$

Lean4

theorem comp_right {f : X → Y} (sep : IsSeparatedMap f) {g : A → X} (cont : Continuous g) (inj : g.Injective) :
    IsSeparatedMap (f ∘ g) := by
  rw [isSeparatedMap_iff_isClosed_diagonal] at sep ⊢
  rw [← inj.preimage_pullbackDiagonal]
  exact sep.preimage (cont.mapPullback cont)

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