comp_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem comp_left {A} {f : X → Y} (sep : IsSeparatedMap f) {g : Y → A} (inj : g.Injective) : IsSeparatedMap (g ∘ f) :=
  fun x₁ x₂ he ↦ sep x₁ x₂ (inj he)

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