comp_iff — Mathlib

English

For suitable morphisms f: X → Y and g: Y → Z, IsSeparated (f ≫ g) is equivalent to IsSeparated f when g is separated.

Русский

Для подходящих морфизмов f: X → Y и g: Y → Z условие IsSeparated (f ≫ g) эквивалентно IsSeparated f, если g разделим.

LaTeX

$$$\text{IsSeparated}(f \circ g) \iff \text{IsSeparated}(f)$, given \ IsSeparated(g).$$

Lean4

theorem comp_iff [IsSeparated g] : IsSeparated (f ≫ g) ↔ IsSeparated f :=
  ⟨fun _ ↦ .of_comp f g, fun _ ↦ inferInstance⟩

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